Documentation ¶
Overview ¶
Package asyncpi provides a simple library to work with π-calculus.
The asyncpi package consists of a parser of asynchronous π-calculus and Go code generator to execute the calculus.
Syntax ¶
The basic syntax of the input language is as follows:
P,Q ::= 0 nil process | P|Q parallel composition of P and Q | (new a)P generation of a with scope P | !P replication of P, i.e. infinite parallel composition P|P|P... | u<v> output of v on channel u | u(x).P input of distinct variables x on u, with continuation P
The input language accepted is slightly more flexible with some syntactic sugar. For instance, consecutive new scope can be grouped together, for example:
(new a,b,c)P
Which is equivalent to:
(new a)(new b)(new c)P
Another optional syntax accepted in the input language is type annotations on the names being created. This feature is mainly designed for code generation. The following annotation attaches the type int to the name i.
(new i:int)P
However, the annotation is only a hint, the type inference may assign i with a different type if its usage does not match the annotation.
(new i:int)i<>
Since i is used as a channel, i cannot be of type int, the annotation is therefore ignored.
Index ¶
- Variables
- func Bind(p *Process) error
- func IsFreeName(x Name) bool
- func IsSameName(x, y Name) bool
- func Reduce1(p Process) (changed bool, err error)
- func Subst(p Process, vs, xs []Name) error
- type ImmutableNameError
- type Name
- type NilProcess
- type Par
- type ParseError
- type Process
- type Recv
- type Repeat
- type Restrict
- type Send
- type TokenPos
- type UnknownProcessError
Examples ¶
Constants ¶
This section is empty.
Variables ¶
Functions ¶
func Bind ¶
Bind takes a parsed process p and returned a process with valid binding.
func IsSameName ¶
IsSameName is a simple comparison operator for Name. A Name x is equal with another Name y when x and y has the same name. This comparison ignores the underlying representation (sort, type, etc.).
func Reduce1 ¶
Reduce1 performs a single step of reduction for Process p.
Types ¶
type ImmutableNameError ¶
type ImmutableNameError struct {
Name Name
}
ImmutableNameError is the type of error when trying to modify a name without setter methods.
func (ImmutableNameError) Error ¶
func (e ImmutableNameError) Error() string
type Name ¶
Name is channel or value.
type NilProcess ¶
type NilProcess struct{}
NilProcess is the inaction process.
func (*NilProcess) Calculi ¶
func (p *NilProcess) Calculi() string
func (*NilProcess) FreeNames ¶
func (n *NilProcess) FreeNames() []Name
FreeNames of NilProcess is defined to be empty.
func (*NilProcess) FreeVars ¶
func (n *NilProcess) FreeVars() []Name
FreeVars of NilProcess is defined to be empty.
func (*NilProcess) String ¶
func (n *NilProcess) String() string
type Par ¶
type Par struct {
Procs []Process
}
Par is parallel composition of P and Q.
func (*Par) FreeNames ¶
FreeNames of Par is the free names of composed processes.
func (*Par) FreeVars ¶
FreeVars of Par is the free names of composed processes.
type ParseError ¶
ParseError is the type of error when parsing an asyncpi process.
func (*ParseError) Error ¶
func (e *ParseError) Error() string
type Process ¶
type Process interface { FreeNames() []Name FreeVars() []Name // Calculi returns the calculi representation. Calculi() string String() string }
Process is process prefixed with action.
func Parse ¶
Parse is the entry point to the asyncpi calculus parser.
Example ¶
This example shows how the parser should be invoked.
proc, err := Parse(strings.NewReader("(new a) (a<v> | a(x).b(y).0 | b<u>)")) if err != nil { fmt.Println(err) // Parse failed } fmt.Println(proc.String())
Output: restrict(a,par[ par[ send(a,[v]) | recv(a,[x]).recv(b,[y]).inact ] | send(b,[u]) ])
type Recv ¶
type Recv struct { Chan Name // Channel to receive from. Vars []Name // Variable expressions. Cont Process // Continuation. }
Recv is input of Vars on channel Chan, with continuation Cont.
func (*Recv) FreeNames ¶
FreeNames of Recv is the channel and FreeNames of the continuation.
func (*Recv) FreeVars ¶
FreeVars of Recv is the channel and FreeVars in continuation minus received variables.
type Repeat ¶
type Repeat struct {
Proc Process
}
Repeat is a replicated Process.
func (*Repeat) FreeNames ¶
FreeNames of Repeat are FreeNames in Proc.
func (*Repeat) FreeVars ¶
FreeVars of Repeat are FreeVars in Proc.
type Restrict ¶
Restrict is scope of Process.
func NewRestrict ¶
NewRestrict creates a new restriction.
func NewRestricts ¶
NewRestricts creates consecutive restrictions from a slice of Names.
func (*Restrict) FreeNames ¶
FreeNames of Restrict are FreeNames in Proc excluding Name.
func (*Restrict) FreeVars ¶
FreeVars of Restrict are FreeVars in Proc.
type Send ¶
Send is output of Vals on channel Chan.
func (*Send) FreeNames ¶
FreeNames of Send is the channel and the Vals.
type TokenPos ¶
TokenPos is a pair of coordinate to identify start of token.
func (TokenPos) CaretDiag ¶
CaretDiag returns the input b with caret to locate error position for diagnosis.
type UnknownProcessError ¶
type UnknownProcessError struct {
Proc Process
}
UnknownProcessError is the type of error when a type switch encounters an unknown Process implementation.
The Process implementation may be valid but the caller does not anticipate or handle it.
func (UnknownProcessError) Error ¶
func (e UnknownProcessError) Error() string
Source Files ¶
Directories ¶
Path | Synopsis |
---|---|
cmd
|
|
asyncpi
Command asyncpi is a REPL frontend for the asyncpi package.
|
Command asyncpi is a REPL frontend for the asyncpi package. |
codegen
|
|
golang
Package golang provides a golang codegen backend for the asyncpi package.
|
Package golang provides a golang codegen backend for the asyncpi package. |
internal
|
|
errors
Package errors provides internal error handlign routines.
|
Package errors provides internal error handlign routines. |
name
Package name provides internal default implementations of the asyncpi Names.
|
Package name provides internal default implementations of the asyncpi Names. |
Package name contains support functions for working with Name.
|
Package name contains support functions for working with Name. |
sortedname
Package sortedname provides a specialised Name implementation associating sorts with a Name.
|
Package sortedname provides a specialised Name implementation associating sorts with a Name. |
Package types declares the types and implements the algorithms for type inference for programs written using the asyncpi package.
|
Package types declares the types and implements the algorithms for type inference for programs written using the asyncpi package. |