cfsm

README

cfsm

nickng/cfsm is a CFSMs library in Go.

Communicating Finite State Machines (CFSMs) or Communicating Automata are formalisims for modelling concurrent processes by Brand and Zafiropulo (1983).

This is an implementation of CFSMs in Go for generating input petri nets for petrify, used in Synthesising choreographies.

Documentation

Overview

Package cfsm is a library for working with Communicating Finite State Machines.

Index

• Constants
• Variables
• type CFSM
  • func (m *CFSM) AddState(s *State)
  • func (m *CFSM) IsEmpty() bool
  • func (m *CFSM) NewFreeState() *State
  • func (m *CFSM) NewState() *State
  • func (m *CFSM) States() []*State
  • func (m *CFSM) String() string
• type Recv
  • func NewRecv(cfsm *CFSM, msg string) *Recv
  • func (r *Recv) Label() string
  • func (r *Recv) SetNext(st *State)
  • func (r *Recv) State() *State
• type Send
  • func NewSend(cfsm *CFSM, msg string) *Send
  • func (s *Send) Label() string
  • func (s *Send) SetNext(st *State)
  • func (s *Send) State() *State
• type State
  • func NewState() *State
  • func (s *State) AddTransition(t Transition)
  • func (s *State) Name() string
  • func (s *State) Transitions() []Transition
• type System
  • func NewSystem() *System
  • func (s *System) NewMachine() *CFSM
  • func (s *System) RemoveMachine(id int)
  • func (s *System) String() string
• type Transition

Examples

• System

Constants

const (
	// FreeStateID is the ID used to identify a State unattached to any CFSM.
	FreeStateID = -1
)

Variables

var (
	// ErrStateUndef is an error when referencing a state that does not exist.
	ErrStateUndef = errors.New("Undefined state")
	// ErrStateAlias is an error when reusing a non-free CFSM state in a
	// different CFSM (aliasing).
	ErrStateAlias = errors.New("State is already attached to a CFSM")
)

Types

type CFSM

type CFSM struct {
	ID      int    // Unique identifier.
	Start   *State // Starting state of the CFSM.
	Comment string // Comments on the CFSM.
	// contains filtered or unexported fields
}

CFSM is a single Communicating Finite State Machine.

func (*CFSM) AddState

func (m *CFSM) AddState(s *State)

AddState adds an unattached State to this CFSM.

func (*CFSM) IsEmpty

func (m *CFSM) IsEmpty() bool

IsEmpty returns true if there are no transitions in the CFSM.

func (*CFSM) NewFreeState

func (m *CFSM) NewFreeState() *State

NewFreeState creates a new free State for this CFSM.

func (*CFSM) NewState

func (m *CFSM) NewState() *State

NewState creates a new State for this CFSM.

func (*CFSM) States

func (m *CFSM) States() []*State

States return states defined in the machine.

func (*CFSM) String

func (m *CFSM) String() string

type Recv

type Recv struct {
	// contains filtered or unexported fields
}

Recv is a receive transition (input).

func NewRecv

func NewRecv(cfsm *CFSM, msg string) *Recv

NewRecv returns a new Recv transition.

func (*Recv) Label

func (r *Recv) Label() string

Label for Recv is "?"

func (*Recv) SetNext

func (r *Recv) SetNext(st *State)

SetNext sets the next state of the Recv transition.

func (*Recv) State

func (r *Recv) State() *State

State returns the State after transition.

type Send

type Send struct {
	// contains filtered or unexported fields
}

Send is a send transition (output).

func NewSend

func NewSend(cfsm *CFSM, msg string) *Send

NewSend returns a new Send transition.

func (*Send) Label

func (s *Send) Label() string

Label for Send is "!"

func (*Send) SetNext

func (s *Send) SetNext(st *State)

SetNext sets the next state of the Send transition.

func (*Send) State

func (s *Send) State() *State

State returns the State after transition.

type State

type State struct {
	ID    int    // Unique identifier.
	Label string // Free form text label.
	// contains filtered or unexported fields
}

State is a state.

func NewState

func NewState() *State

NewState creates a new State independent from any CFSM.

func (*State) AddTransition

func (s *State) AddTransition(t Transition)

AddTransition adds a transition to the current State.

func (*State) Name

func (s *State) Name() string

Name of a State is a unique string to identify the State.

func (*State) Transitions

func (s *State) Transitions() []Transition

Transitions returns a list of transitions.

type System

type System struct {
	sync.Mutex
	CFSMs   []*CFSM // Individual CFSMs in the communicating system.
	Comment string  // Comments on the System.
}

System is a set of CFSMs.

Example

To use the CFSM library, first create a system of CFSMs. From the system, create machines (i.e. CFSMs) for the system. Add states to the machines, and attach transitions to the states. Finally set initial state of each machine.

// Create a new system of CFSMs.
sys := NewSystem()
alice := sys.NewMachine() // CFSM Alice
alice.Comment = "Alice"

bob := sys.NewMachine() // CFSM Bob
bob.Comment = "Bob"

a0 := alice.NewState()
a1 := alice.NewState()
a01 := NewSend(bob, "int")
a01.SetNext(a1)
a0.AddTransition(a01) // Add a transition from a0 --> a1.

b0 := bob.NewState()
b1 := bob.NewState()
b01 := NewRecv(alice, "int")
b01.SetNext(b1)
b0.AddTransition(a01) // Add a transition from b0 --> b1.

// Set initial states of alice and bob.
alice.Start = a0
bob.Start = b0

func NewSystem

func NewSystem() *System

NewSystem returns a new communicating system

func (*System) NewMachine

func (s *System) NewMachine() *CFSM

NewMachine creates a new CFSM in the communicating system and returns it.

func (*System) RemoveMachine

func (s *System) RemoveMachine(id int)

RemoveMachine removes a CFSM with the given id from System.

func (*System) String

func (s *System) String() string

type Transition

type Transition interface {
	Label() string // Label is the marking on the transition.
	State() *State // State after transition.
}

Transition is a transition from a State to another State.