README
¶
asyncpi 
An implementation of asynchronous π-calculus in Go.
The basic syntax accept is given below, for details (including syntactic sugar), see godoc.
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
Install
go get go.nickng.io/asyncpi
License
asyncpi is licensed under the Apache License
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 ¶
var ErrInvalid = errors.New("invalid argument")
Functions ¶
func IsFreeName ¶
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.).
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 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.
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]) ])
func SimplifyBySC ¶
SimplifyBySC simplifies a Process p by structural congruence rules.
It applies functions to (1) remove unnecessary Restrict, and (2) remove superfluous inact.
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.
type Repeat ¶
type Repeat struct {
Proc Process
}
Repeat is a replicated Process.
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.
type Send ¶
Send is output of Vals on channel Chan.
type TokenPos ¶
TokenPos is a pair of coordinate to identify start of token.
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. |