pifra

package module
v0.0.4 Latest Latest
Warning

This package is not in the latest version of its module.

 Go to latest Published: Aug 8, 2021 License: MIT Imports: 15 Imported by: 0

README

pifra - Pi-Calculus Fresh-Register Automata

pifra is a tool for generating labelled transition systems (LTS) of pi-calculus models represented by fresh-register automata (FRA).

The LTS is generated according to the xπ-calculus FRA transition relation described in the paper Fresh-Register Automata by Nikos Tzevelekos. The LTS is minimised by normalising each explored state based on equivalance rules.

This work was carried out as part of a master's dissertation with Vasileios Koutavas at Trinity College Dublin.

Installation

go get -u github.com/basil-conto/pifra/pifra

go get downloads the package and its dependencies to $GOPATH/src and creates an executable in $GOPATH/bin.

Command-line interface

pifra --help

pifra generates labelled transition systems (LTS) of
pi-calculus models represented by fresh-register automata.

Usage:
pifra [OPTION...] FILE

Options:
  -n, --max-states int         maximum number of states explored (default 20)
  -r, --max-registers int      maximum number of registers (default is unlimited)
  -d, --disable-gc             disable garbage collection
  -i, --interactive            inspect interactively the LTS in a prompt
  -o, --output string          output the LTS to a file (default format is the Graphviz DOT language)
  -t, --output-tex             output the LTS file with LaTeX labels for use with dot2tex
  -p, --output-pretty          output the LTS file in a pretty-printed format
  -s, --output-states          output state numbers instead of configurations for the Graphviz DOT file
  -l, --output-layout string   layout of the GraphViz DOT file, e.g., "rankdir=TB; margin=0;"
  -q, --quiet                  do not print or output the LTS
  -v, --stats                  print LTS generation statistics
  -h, --help                   show this help message and exit

Pi-calculus models

Syntax
P,Q ::=
      | a(b).P     input
      | <a>'b.P    output
      | [a=b]P     equality
      | [a!=b]P    inequality
      | $a.P       restriction
      | P + Q      summation
      | P | Q      composition
      | p(a)       process
      | 0          inaction

Pdef ::= p(a) = P

Pdef...
Pundecl
Example models

The below and additional pi-calculus models can be found in test/.

fresh.pi

$x.a'<x>.b'<x>.0 | b(y).0

ping1.pi

P = a(x).x'<x>.0 | P
P

tzevelekos.pi

P(a,b) = a'<b>.$c.P(b,c)
$b.P(a,b)

vk-inf-st3.pi

P(a) =  a(x).$y.( x'<y>.0  |  b(z).[z=y] P(a) )
P(a)

password.pi

GenPass(requestNewPass) = requestNewPass(x). $pass. x'<pass>.0

KeepSecret(requestNewPass) = $p. requestNewPass'<p>. p(pass). ( StoreSecret(pass) | TestSecret(pass) )

StoreSecret(pass) = $secret. pass'<secret>. StoreSecret(pass)

TestSecret(pass) = pub(x). pass(secret). ( TestSecret(pass) + [x=secret] _BAD'<_BAD>.0 )

$requestNewPass. (GenPass(requestNewPass)  |  KeepSecret(requestNewPass))

LTS output

The below and additional LTS outputs can be found in test/.

Input model

fresh.pi

$x.a'<x>.b'<x>.0 | b(y).0
Pretty-printed LTS
pifra fresh.pi

s0 = {(1,#1),(2,#2)} |- (#2(&2).0 | $&1.#1'<&1>.#2'<&1>.0)
s0  2 1   s1 = {(1,#1),(2,#2)} |- $&1.#1'<&1>.#2'<&1>.0
s0  2 2   s1 = {(1,#1),(2,#2)} |- $&1.#1'<&1>.#2'<&1>.0
s0  2 3*  s1 = {(1,#1),(2,#2)} |- $&1.#1'<&1>.#2'<&1>.0
s0  1'1^  s2 = {(1,#1),(2,#2)} |- (#2'<#1>.0 | #2(&1).0)
s1  1'1^  s3 = {(1,#1),(2,#2)} |- #2'<#1>.0
s2  2'1   s4 = {(2,#2)} |- #2(&1).0
s2  2 1   s3 = {(1,#1),(2,#2)} |- #2'<#1>.0
s2  2 2   s3 = {(1,#1),(2,#2)} |- #2'<#1>.0
s2  2 3*  s3 = {(1,#1),(2,#2)} |- #2'<#1>.0
s2  t     s5 = {} |- 0
s3  2'1   s5 = {} |- 0
s4  2 2   s5 = {} |- 0
s4  2 1*  s5 = {} |- 0
output meaning
{} ⊢ P configuration
#1 free name
&1 bound name
1 1 known input
1'1 known output
1 1* fresh input
1 1^ fresh output
t tau step
GraphViz DOT LTS

The LTS can be outputted as a GraphViz DOT graph description language.

pifra -o lts.dot fresh.pi
cat lts.dot

digraph {
    s0 [peripheries=2,label="{(1,#1),(2,#2)} ⊢
(#2(&2).0 | $&1.#1'<&1>.#2'<&1>.0)"]
    s1 [label="{(1,#1),(2,#2)} ⊢
$&1.#1'<&1>.#2'<&1>.0"]
    s2 [label="{(1,#1),(2,#2)} ⊢
(#2'<#1>.0 | #2(&1).0)"]
    s3 [label="{(1,#1),(2,#2)} ⊢
#2'<#1>.0"]
    s4 [label="{(2,#2)} ⊢
#2(&1).0"]
    s5 [label="{} ⊢
0"]

    s0 -> s1 [label="2 1"]
    s0 -> s1 [label="2 2"]
    s0 -> s1 [label="2 3●"]
    s0 -> s2 [label="1' 1⊛"]
    s1 -> s3 [label="1' 1⊛"]
    s2 -> s4 [label="2' 1"]
    s2 -> s3 [label="2 1"]
    s2 -> s3 [label="2 2"]
    s2 -> s3 [label="2 3●"]
    s2 -> s5 [label="τ"]
    s3 -> s5 [label="2' 1"]
    s4 -> s5 [label="2 2"]
    s4 -> s5 [label="2 1●"]
}

Using the GraphViz toolset, a visualisation of the LTS can be generated.

pifra -o lts.dot fresh.pi
dot -Tpdf -o lts.pdf lts.dot
GraphViz DOT with LaTeX labels LTS

The LTS can be outputted as a dot2tex-compatible DOT file, which uses LaTeX labels.

pifra -t -o lts.dot fresh.pi
dot2tex -o lts.tex lts.dot
pdflatex lts.tex

State numbers can be outputted instead of configurations.

pifra -st -o lts.dot fresh.pi
dot2tex -o lts.tex lts.dot
pdflatex lts.tex

Documentation

Index

Constants

View Source 
const APOSTROPHE = 57359
View Source 
const COMMA = 57353
View Source 
const COMMENT = 57357
View Source 
const DOLLARSIGN = 57360
View Source 
const DOT = 57356
View Source 
const EQUAL = 57354
View Source 
const EXCLAMATION = 57362
View Source 
const LANGLE = 57349
View Source 
const LBRACKET = 57347
View Source 
const LOWER_THAN_LBRACKET = 57364
View Source 
const LOWPREC = 57363
View Source 
const LSQBRACKET = 57351
View Source 
const NAME = 57346
View Source 
const PLUS = 57361
View Source 
const RANGLE = 57350
View Source 
const RBRACKET = 57348
View Source 
const RSQBRACKET = 57352
View Source 
const VERTBAR = 57355
View Source 
const ZERO = 57358

Variables

View Source 
var DeclaredProcs map[string]DeclaredProcess

DeclaredProcs is a map of name -> (process, parameters).

Functions

func DoAlphaConversion 

func DoAlphaConversion(elem Element)

DoAlphaConversion renames bound names to names appropriate to their scope.

func GetAllFreeNames 

func GetAllFreeNames(elem Element) []string

GetAllFreeNames returns all fresh names in the AST.

func InteractiveMode 

func InteractiveMode(flags Flags)

InteractiveMode allows the user to inspect interactively the LTS in a prompt.

func Log 

func Log(strs ...string)

Log prints debug statements.

func OutputMode 

func OutputMode(flags Flags) error

OutputMode generates an LTS from the pi-calculus program file and either writes the output to a file, or prints the output if an output file is not specified.

func PrettyPrintAst 

func PrettyPrintAst(elem Element) string

PrettyPrintAst returns a string containing the pi-calculus syntax of the AST.

func PrettyPrintConfiguration 

func PrettyPrintConfiguration(conf Configuration) string

PrettyPrintConfiguration returns a pretty printed string of the configuration.

func RegisterGobs 

func RegisterGobs()

RegisterGobs registers concrete types implementing the Element interface for encoding as binary gobs.

Types

type Configuration 

type Configuration struct {
	Process   Element
	Registers Registers
	Label     Label
}

type DeclaredProcess 

type DeclaredProcess struct {
	Process    Element
	Parameters []string
}

type EdgeTemplate 

type EdgeTemplate struct {
	Source      string
	Destination string
	Label       string
}

type ElemEquality 

type ElemEquality struct {
	Inequality bool
	NameL      Name
	NameR      Name
	Next       Element
}

func (*ElemEquality) Type 

func (e *ElemEquality) Type() ElementType

type ElemInput 

type ElemInput struct {
	Channel Name
	Input   Name
	Next    Element
}

func (*ElemInput) Type 

func (e *ElemInput) Type() ElementType

type ElemNil 

type ElemNil struct{}

func (*ElemNil) Type 

func (e *ElemNil) Type() ElementType

type ElemOutput 

type ElemOutput struct {
	Channel Name
	Output  Name
	Next    Element
}

func (*ElemOutput) Type 

func (e *ElemOutput) Type() ElementType

type ElemParallel 

type ElemParallel struct {
	ProcessL Element
	ProcessR Element
}

func (*ElemParallel) Type 

func (e *ElemParallel) Type() ElementType

type ElemProcess 

type ElemProcess struct {
	Name       string
	Parameters []Name
}

func (*ElemProcess) Type 

func (e *ElemProcess) Type() ElementType

type ElemRestriction 

type ElemRestriction struct {
	Restrict Name
	Next     Element
}

func (*ElemRestriction) Type 

func (e *ElemRestriction) Type() ElementType

type ElemRoot 

type ElemRoot struct {
	Next Element
}

func (*ElemRoot) Type 

func (e *ElemRoot) Type() ElementType

type ElemSum 

type ElemSum struct {
	ProcessL Element
	ProcessR Element
}

func (*ElemSum) Type 

func (e *ElemSum) Type() ElementType

type Element 

type Element interface {
	Type() ElementType
}

func InitProgram 

func InitProgram(program []byte) (Element, error)

InitProgram parses the byte array and returns the root undeclared process.

func InitRootAst 

func InitRootAst(elem Element) Element

InitRootAst performs alpha-conversion and adds a root element to the AST as the head, for use in the transition relation.

type ElementType 

type ElementType int
const (
	ElemTypNil ElementType = iota
	ElemTypOutput
	ElemTypInput
	ElemTypMatch
	ElemTypRestriction
	ElemTypSum
	ElemTypParallel
	ElemTypProcess

	ElemTypRoot
)

type Flags 

type Flags struct {
	InteractiveMode bool

	RegisterSize int
	MaxStates    int
	DisableGC    bool

	InputFile  string
	OutputFile string

	GVLayout       string
	GVOutputStates bool
	GVTex          bool

	Pretty     bool
	Gob        bool
	Statistics bool

	Quiet bool
}

Flags are the user-specified flags for the command line.

type Label 

type Label struct {
	Symbol  Symbol
	Symbol2 Symbol
}

func (Label) PrettyPrintGraph 

func (l Label) PrettyPrintGraph() string

type Lts 

type Lts struct {
	States      map[int]Configuration
	Transitions []Transition

	RegSizeReached map[int]bool

	StatesExplored  int
	StatesGenerated int
}

type Name 

type Name struct {
	Name string
	Type NameType
}

type NameType 

type NameType int
const (
	Free NameType = iota
	Bound
)

type Registers 

type Registers struct {
	Size      int
	Registers map[int]string
}

func (*Registers) AddEmptyName 

func (reg *Registers) AddEmptyName()

AddEmptyName increments all labels by one while retaining mapping to their name and leaves an empty name (#) at label 1. #+o = {(1, #)} U {(i+1, v′) | (i, v′) E o}.

func (*Registers) GetLabel 

func (reg *Registers) GetLabel(name string) int

GetLabel returns register label corresponding to the name.

func (*Registers) GetName 

func (reg *Registers) GetName(label int) string

GetName returns register name corresponding to the label.

func (*Registers) Labels 

func (reg *Registers) Labels() []int

Labels returns register labels in sorted order.

func (*Registers) RemoveMax 

func (reg *Registers) RemoveMax()

RemoveMax removes a free name from the register at the register size + 1 and decrements the register size. Undos UpdateMax.

func (*Registers) UpdateMax 

func (reg *Registers) UpdateMax(freeName string) int

UpdateMax adds a free name to the register at the register size + 1 and increments the register size. σ+v = σ U {(|σ|+1, v)}.

func (*Registers) UpdateMin 

func (reg *Registers) UpdateMin(name string, freshNames []string) int

UpdateMin updates the register with a name at the minimum label where it does not exist in the set of free names.

type Symbol 

type Symbol struct {
	Type  SymbolType
	Value int
}

type SymbolType 

type SymbolType int
const (
	SymbolTypTau SymbolType = iota
	SymbolTypInput
	SymbolTypOutput
	SymbolTypFreshInput
	SymbolTypFreshOutput
	SymbolTypKnown
)

type Transition 

type Transition struct {
	Source      int
	Destination int
	Label       Label
}

type VertexTemplate 

type VertexTemplate struct {
	State  string
	Config string
	Layout string
}

Source Files

View all Source files

Directories

Path Synopsis

Jump to

Keyboard shortcuts

? : This menu
/ : Search site
f or F : Jump to
y or Y : Canonical URL
go.dev uses cookies from Google to deliver and enhance the quality of its services and to analyze traffic. Learn more.