trait AtomicProcess extends MetadataAtomicProcess

case class AtomicProcessIsCompositeException[KeyT](pii: PiInstance[KeyT], process: String) extends PiException[KeyT] with HasPiInstance[KeyT] with Product with Serializable

case class Chan(s: String) extends PiObject with Product with Serializable

A pi-calculus channel.

These may be used for communication, they may be communicated themselves, and they are also used as variables.

For instance, channels are used as variables to create patterns of expected inputs and outputs. For example, a process may expect a pair PiPair(Chan(X),Chan(Y)) as input. Each of the channels X and Y will (should) eventually be instantiated to a resource.

e.g. receiving input a(X).0 from a matching output 'a<"Hello">.0 creates the instatiation X --> "Hello".

We apply these instantiations to the pattern PiPair(Chan(X),Chan(Y)) until the pattern contains no channels/variables. We then know that the input is available and the process can be executed (pending all other inputs as well). A process would never receive and/or do anything useful with a pi-calculus channel.

s: The name of the channel.

case class ChanMap(map: Map[Chan, PiObject] = Map()) extends Product with Serializable

An instantion map of channels (Chan) to PiObject.

They are used for substitution (especially in continuations) and to instantiate patterns.

A ChanMap is a wrapper around a regular, immutable map.

map: A mapping of Chans to PiObjects.

sealed trait ChannelTerm extends Term

A ChannelTerm is a Term that depends on a particular channel to operate.

A ChannelTerm is a Term that depends on a particular channel to operate. Essentially the equivalent of a pi-calculus continuation.

trait CompositeProcess extends PiProcess

case class Devour(channel: Chan, value: Chan) extends Input with Product with Serializable

c(v).0 Receives any PiObject through channel c and maps it to channel v.

case class DummyComposition(name: String, i: String, o: String, n: String) extends CompositeProcess with Product with Serializable

case class DummyProcess(name: String, outChan: String, inputs: Seq[(PiObject, String)]) extends AtomicProcess with Product with Serializable

sealed trait HasPiInstance[KeyT] extends PiException[KeyT]

case class In(channel: Chan, value: Chan, cont: Term) extends Input with Product with Serializable

c(v).cont Receives an atomic PiObject (channel or item) through channel c, maps it to channel v, applies the resulting substitution to the continuation and returns the result.

sealed trait Input extends ChannelTerm

Input Terms for proofs-as-processes compositions.

case class LeftOut(channel: Chan, lchan: Chan, cont: Term) extends Output with Product with Serializable

'c<lc>.cont Optional left output.

'c<lc>.cont Optional left output. We do not have sums here. Optional communication happens through pairs of channels as the parallel one. However, WithIn only anticipates a PiLeft or a PiRight. This returns a PiLeft with a fresh channel to receive the actual resource from.

Note that this is different from the proofs-as-processes way of handling optional communication. In that, channel polarity gets flipped. i.e. the output channel *receives* the 2 channels for each of the options. We avoid this here.

trait MetadataAtomicProcess extends PiProcess

case class NoResultException[KeyT](pii: PiInstance[KeyT]) extends PiException[KeyT] with HasPiInstance[KeyT] with Product with Serializable

case class NoSuchInstanceException[KeyT](id: KeyT) extends PiException[KeyT] with Product with Serializable

case class Out(channel: Chan, a: PiObject) extends Output with Product with Serializable

'c.0 Sends a PiObject through a channel.

sealed trait Output extends ChannelTerm

Output Terms for proofs-as-processes compositions.

case class ParIn(channel: Chan, lvalue: Chan, rvalue: Chan, left: Term, right: Term) extends Input with Product with Serializable

c(lv,rv).(left | right) Parallel input.

c(lv,rv).(left | right) Parallel input. Receives a PiPair, instantiates each continuation appropriately and returns them.

case class ParInI(channel: Chan, lvalue: Chan, rvalue: Chan, cont: Term) extends Input with Product with Serializable

c(lv,rv).cont Parallel input with single continuation.

c(lv,rv).cont Parallel input with single continuation. This occurs from the application of the Par CLL rule.

case class ParOut(channel: Chan, lchan: Chan, rchan: Chan, left: Term, right: Term) extends Output with Product with Serializable

'c<lc,rc>.(left | right) Parallel output.

'c<lc,rc>.(left | right) Parallel output. In proofs-as-processes, parallel communication (i.e. of a pair of objects) happens in 2 stages: 1) Use a common channel to send 2 new channels, one for the left side of the pair and one for the right. 2) Communicate each part of the pair through its respective channel. This performs the output for the first stage. Creates fresh versions of lc and rc and then sends them out as a pair.

sealed trait PiAtomicProcessEvent[KeyT] extends PiEvent[KeyT]

PiEvents which are associated with a specific AtomicProcess call.

KeyT: The type used to identify PiInstances.

case class PiCall(name: String, args: Seq[Chan]) extends Term with Product with Serializable

A call to an atomic process in the composition.

name: the name of the process being called
args: the (channel) parameters given

case class PiCut(z: Chan, lchan: Chan, rchan: Chan, left: Term, right: Term) extends Term with Product with Serializable

Proofs-as-processes cut pattern.

Proofs-as-processes cut pattern. Substitutes channels lc in left and rc in right with a fresh version of z, then adds them to the state. In a proofs-as-processes generated composition, one (currently the left) will be an input and the other will be an output, so this will force them to communicate with each other. It is nice, however, that polymorphism on withTerm allows us to not specify which is which, so we are closer to the pure pi-calculus.

sealed trait PiEvent[KeyT] extends AnyRef

Super-class for any PiProcess events which take place during workflow execution or simulation.

Super-class for any PiProcess events which take place during workflow execution or simulation. These can be understood as being divided in 2 ways (into 4 categories):

By Level:

Workflow Level: for events concerning CompositeProcess begun with a call to ProcessExecutor.execute. These are keyed by at least the ID of the corresponding PiInstance.
Atomic Process Level: for events concerning AtomicProcess that were called by an ProcessExecutor during the execution of a Workflow Level CompositeProcess. These are keyed by both the PiInstance ID and the individual call ID (which uniquely enumerates each call made by a PiInstance).

By Type:

Start: these events mark the start of process execution.
End: these events mark the termination of process execution, either by successful completion along with a result or by a failure. These should always be preceded by a corresponding start/call event.

KeyT: The type used to identify PiInstances.

case class PiEventCall[KeyT](id: KeyT, ref: Int, p: MetadataAtomicProcess, args: Seq[PiObject], metadata: PiMetadataMap = PiMetadata()) extends PiAtomicProcessEvent[KeyT] with Product with Serializable

Denotes the start of a AtomicProcess execution made during the execution of a parent CompositeProcess.

KeyT: The type used to identify PiInstances.
id: PiInstance ID for the parent CompositeProcess.
ref: Enumerated ID for this AtomicProcess call, unique for this PiInstance.
p: Reference to AtomicProcess called.
args: Parameter values for the AtomicProcess call.
metadata: Metadata object.

sealed trait PiEventCallEnd[KeyT] extends PiAtomicProcessEvent[KeyT]

Abstract superclass for all PiAtomicProcessEvent which denote the termination of an AtomicProcess call.

KeyT: The type used to identify PiInstances.

sealed trait PiEventFinish[KeyT] extends PiEvent[KeyT]

Abstract superclass for all PiEvents which denote the termination of a PiInstance.

case class PiEventIdle[KeyT](i: PiInstance[KeyT], metadata: PiMetadataMap = PiMetadata()) extends PiEvent[KeyT] with PiEventFinish[KeyT] with Product with Serializable

Denotes the completion of all reductions and process calls.

Denotes the completion of all reductions and process calls. We are waiting for at least one process call to complete. This is useful in simulations so we know when to progress in virtual time.

KeyT: The type used to identify PiInstances.
i: PiInstance representing the current state.
metadata: Metadata object.

Note: Not all executor implementations fire this event.

case class PiEventResult[KeyT](i: PiInstance[KeyT], res: Any, metadata: PiMetadataMap = PiMetadata()) extends PiEvent[KeyT] with PiEventFinish[KeyT] with Product with Serializable

Denotes the successful completion of execution of a CompositeProcess.

KeyT: The type used to identify PiInstances.
i: PiInstance representing the terminal state of this PiProcess.
res: The corresponding result object of this CompositeProcess.
metadata: Metadata object.

case class PiEventReturn[KeyT](id: KeyT, ref: Int, result: Any, metadata: PiMetadataMap = PiMetadata()) extends PiAtomicProcessEvent[KeyT] with PiEventCallEnd[KeyT] with Product with Serializable

Denotes the successful completion of execution of a AtomicProcess.

KeyT: The type used to identify PiInstances.
id: PiInstance ID for the parent CompositeProcess.
ref: Enumerated ID for this AtomicProcess call, unique for this PiInstance.
result: Object returned by this execution of the AtomicProcess.
metadata: Metadata object.

case class PiEventStart[KeyT](i: PiInstance[KeyT], metadata: PiMetadataMap = PiMetadata()) extends PiEvent[KeyT] with Product with Serializable

Denotes the start of execution of a CompositeProcess.

KeyT: The type used to identify PiInstances.
i: PiInstance representing the start state of this PiProcess.
metadata: Metadata object.

sealed abstract class PiException[KeyT] extends Exception

sealed trait PiFailure[KeyT] extends PiEvent[KeyT]

Denotes that the corresponding PiInstance failed to complete execution.

KeyT: The type used to identify PiInstances.

case class PiFailureAtomicProcessException[KeyT](id: KeyT, ref: Int, message: String, trace: Array[StackTraceElement], metadata: PiMetadataMap) extends PiAtomicProcessEvent[KeyT] with PiFailure[KeyT] with PiEventCallEnd[KeyT] with Product with Serializable

Denotes that a AtomicProcess call was terminated by encountering an Exception from which it could not recover.

KeyT: The type used to identify PiInstances.
id: PiInstance ID for the parent CompositeProcess.
ref: Enumerated ID for this AtomicProcess call, unique for this PiInstance.
message: Message of the Exception encountered.
trace: A full trace of the encountered Exception.
metadata: Metadata object.

case class PiFailureAtomicProcessIsComposite[KeyT](i: PiInstance[KeyT], process: String, metadata: PiMetadataMap = PiMetadata()) extends PiFailure[KeyT] with PiEventFinish[KeyT] with Product with Serializable

The ProcessExecutor attempted to dispatch a CompositeProcess to the AtomicProcessExecutor, this is likely because it was unable to be fully reduced.

(Note: This indicates the workflow has not been properly constructed)

KeyT: The type used to identify PiInstances.
i: PiInstance representing the final state of this PiProcess.
process: Name of the unexpected CompositeProcess.
metadata: Metadata object.

case class PiFailureExceptions[KeyT](id: KeyT, message: String, trace: Array[StackTraceElement], metadata: PiMetadataMap) extends PiFailure[KeyT] with PiEventFinish[KeyT] with Product with Serializable

At least one AtomicProcess called by this PiInstance encountered irrecoverable exceptions during execution.

KeyT: The type used to identify PiInstances.
id: ID of corresponding PiInstance.
message: Message of Exception encountered by the AtomicProcess.
trace: A full trace of the encountered Exception.
metadata: Metadata object.

case class PiFailureNoResult[KeyT](i: PiInstance[KeyT], metadata: PiMetadataMap = PiMetadata()) extends PiFailure[KeyT] with PiEventFinish[KeyT] with Product with Serializable

The ProcessExecutor could not provide a result after completing execution of this PiInstance.

KeyT: The type used to identify PiInstances.
i: PiInstance representing the final state of this PiProcess.
metadata: Metadata object.

case class PiFailureNoSuchInstance[KeyT](id: KeyT, metadata: PiMetadataMap = PiMetadata()) extends PiFailure[KeyT] with PiEventFinish[KeyT] with Product with Serializable

A ProcessExecutor could not initiate execution of this PiInstance because it did not have a record of a prior initialisation using ProcessExecutor.init.

KeyT: The type used to identify PiInstances.
id: Unrecognised PiInstance ID attempting execution.
metadata: Metadata object.

case class PiFailureUnknownProcess[KeyT](i: PiInstance[KeyT], process: String, metadata: PiMetadataMap = PiMetadata()) extends PiFailure[KeyT] with PiEventFinish[KeyT] with Product with Serializable

The ProcessExecutor could not complete execution of this PiInstance because it required execution of an AtomicProcess unknown to the ProcessExecutor.

(Note: This indicates the ProcessExecutor has been incorrectly configured)

KeyT: The type used to identify PiInstances.
i: PiInstance representing the final state of this PiProcess.
process: Name of the process that could not be identified.
metadata: Metadata object.

case class PiFuture(fun: String, outChan: Chan, args: Seq[PiResource]) extends Product with Serializable

Represents a pending call to an atomic process in 2 situations: 1) A call has been encountered in the workflow, but we are waiting for the inputs to arrive.

Represents a pending call to an atomic process in 2 situations: 1) A call has been encountered in the workflow, but we are waiting for the inputs to arrive. 2) The inputs have arrived, we have made the call to the actual process, and we are waiting for it to return.

fun: the name of the process
outChan: the channel through which we should send the output when it arrives
args: the process inputs, each including a pattern of the input and the corresponding channel it will arrive through

case class PiInstance[T](id: T, called: Seq[Int], process: PiProcess, state: PiState) extends Product with Serializable

trait PiInstanceMutableStore[T] extends AnyRef

trait PiInstanceStore[T] extends AnyRef

case class PiItem[+A](i: A) extends PiObject with Product with Serializable

A resource that can be communicated through pi-calculus channels.

This represents a resource (actually a container) that is treated as untyped in practice, but its type corresponds to a CLL proposition. It is untyped so we can freely send it through pi-calculus channels without the compiler complaining. Its correspondence with CLL ensures we can type cast it without error when we need to obtain the actual resource.

i: The actual resource being carried.

case class PiLeft(l: PiObject) extends PiObject with Product with Serializable

Representation of a left selection of an option.

This is used in LeftOut to build an output that selects the left option. In CLL, it corresponds to a A (+) B output type generated by the (+)L rule.

l: The object representing the selected type (A).

sealed trait PiObject extends AnyRef

A PiObject is a custom structure representing an object being passed around a pi-calculus workflow.

A PiObject is a custom structure representing an object being passed around a pi-calculus workflow. It mirrors the propositional CLL types, but is untyped at the item level.

A PiObject can be:

A pi-calculus channel: Chan.
An item: PiItem.
A pair: PiPair.
An option: PiOpt.
A Left or a Right selection: PiLeft and PiRight

case class PiOpt(l: PiObject, r: PiObject) extends PiObject with Product with Serializable

A sum (option) between two PiObjects.

Only one of the two PiObjects will be used, similarly to the Either type and corresponding to the A (+) B type in CLL.

l: The first (left) option.
r: The second (right) option.

case class PiPair(l: PiObject, r: PiObject) extends PiObject with Product with Serializable

A pair of PiObjects.

This corresponds to the A (x) B type in CLL.

l: The first (left) element of the pair.
r: The second (right) element of the pair.

sealed trait PiProcess extends AnyRef

A trait corresponding to any process that can be executed within our framework.

A trait corresponding to any process that can be executed within our framework. The specification generally follows the proofs-as-processes format, with PiObject patterns representing CLL types, paired with strings representing the channel names. *

trait PiProcessStore extends AnyRef

case class PiResource(obj: PiObject, c: Chan) extends Product with Serializable

A pi-calculus resource (CLL type) annotated with a channel that carries it.

This effectively corresponds to an annotated CLL term in a sequent.

obj: The PiObject corresponding to the (type of that) resource.
c: The channel that carries the resource.

case class PiRight(r: PiObject) extends PiObject with Product with Serializable

Representation of a right selection of an option.

This is used in RightOut to build an output that selects the right option. In CLL, it corresponds to a A (+) B output type generated by the (+)R rule.

r: The object representing the selected type (B).

case class PiState(inputs: Map[Chan, Input], outputs: Map[Chan, Output], calls: List[PiFuture], threads: Map[Int, PiFuture], threadCtr: Int, freshCtr: Int, processes: Map[String, PiProcess], resources: ChanMap) extends Product with Serializable

This is the pi-calculus state of a running workflow.

We separate inputs from outputs to make searching for matching channels more efficient. We could have everything in one list like PiLib does.

inputs: a map of Input type continuations based on their primary channels
outputs: a map of Output type continuations based on their primary channels
calls: a list of processes that have been called but the inputs haven't arrived yet
threads: a map of processes that have been called and whose results we want. The calls to the actual processes should happen outside the PiState by a process executor, so that things are kept clean and independent here. Each call has a unique reference number so that results don't clash.
threadCtr: an integer to help create unique reference numbers for threads
freshCtr: an integer to help create unique (fresh) channel names
processes: a map of available processes, both atomic and composite, so that we know how to handle calls when they occur
resources: a ChanMap of unhandled resources. We try to keep this as clean as possible, so that it only contains resources that need to be received by a pending call (though this is not guaranteed, we might get some leftover garbage in here as well).

trait PiStateTester extends AnyRef

class RemoteException[KeyT] extends PiException[KeyT]

class RemoteProcessException[KeyT] extends PiException[KeyT]

case class RightOut(channel: Chan, rchan: Chan, cont: Term) extends Output with Product with Serializable

'c<rc>.cont Optional right output.

'c<rc>.cont Optional right output. We do not have sums here. Optional communication happens through pairs of channels as the parallel one. However, WithIn only anticipates a PiLeft or a PiRight. This returns a PiRight with a fresh channel to receive the actual resource from.

Note that this is different from the proofs-as-processes way of handling optional communication. In that, channel polarity gets flipped. i.e. the output channel *receives* the 2 channels for each of the options. We avoid this here.

case class SimpleInstanceStore[T](m: Map[T, PiInstance[T]]) extends PiInstanceStore[T] with Product with Serializable

case class SimpleProcessStore(m: Map[String, PiProcess]) extends PiProcessStore with Product with Serializable

sealed trait Term extends AnyRef

A Term is a pi-calculus pattern that can be encountered in a proofs-as-processes composition.

case class UnknownProcessException[KeyT](pii: PiInstance[KeyT], process: String) extends PiException[KeyT] with HasPiInstance[KeyT] with Product with Serializable

case class WithIn(channel: Chan, lvalue: Chan, rvalue: Chan, left: Term, right: Term) extends Input with Product with Serializable

c(lv,rv).(left + right) Optional input.

c(lv,rv).(left + right) Optional input. Can only receive a PiLeft or PiRight. Instantiates and returns the corresponding continuation.

Packages

pew

package pew

Type Members

Value Members

Ungrouped

Packages

pew 

package pew

Type Members

Value Members

Ungrouped

pew