sesstype

package
Version: v1.0.0 Latest Latest
Warning

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

Go to latest
Published: Jan 10, 2019 License: Apache-2.0 Imports: 8 Imported by: 0

Documentation

Overview

Package sesstype encapsulates representation of session types As opposed to role-based session types, this representation is channel-based. In particular, sending and receiving both keep track of the role and channel involved.

Index

Constants

View Source
const (
	NoOp op = iota
	NewChanOp
	SendOp
	RecvOp
	EndOp
)

Different operations/actions available in session.

View Source
const STOP = "STOP"

STOP is the 'close' message.

Variables

This section is empty.

Functions

func CountNodes

func CountNodes(root Node) int

func PrintNodeSummary

func PrintNodeSummary(session *Session)

func SessionCountNodes

func SessionCountNodes(session *Session) map[string]int

func StringRecursive

func StringRecursive(node Node) string

Types

type CFSMs

type CFSMs struct {
	Sys    *cfsm.System
	Chans  map[Role]*cfsm.CFSM
	Roles  map[Role]*cfsm.CFSM
	States map[*cfsm.CFSM]map[string]*cfsm.State
}

CFSMs captures a CFSM system syserated from a Session.

func NewCFSMs

func NewCFSMs(s *Session) *CFSMs

func (*CFSMs) PrintSummary

func (sys *CFSMs) PrintSummary()

PrintSummary shows the statistics of the CFSM syseration.

func (*CFSMs) WriteTo

func (sys *CFSMs) WriteTo(w io.Writer) (int64, error)

WriteTo implementers io.WriterTo interface.

type Chan

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

Chan is a typed channel in a session.

func (Chan) Name

func (ch Chan) Name() string

Return a name of channel.

func (Chan) Role

func (ch Chan) Role() Role

func (Chan) Type

func (ch Chan) Type() types.Type

Return the payload type of channel.

func (Chan) Value

func (ch Chan) Value() ssa.Value

type EmptyBodyNode

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

func (*EmptyBodyNode) Append

func (e *EmptyBodyNode) Append(node Node) Node

func (*EmptyBodyNode) Child

func (e *EmptyBodyNode) Child(i int) Node

func (*EmptyBodyNode) Children

func (e *EmptyBodyNode) Children() []Node

func (*EmptyBodyNode) Kind

func (e *EmptyBodyNode) Kind() op

func (*EmptyBodyNode) String

func (e *EmptyBodyNode) String() string

type EndNode

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

func (*EndNode) Append

func (e *EndNode) Append(n Node) Node

func (*EndNode) Chan

func (e *EndNode) Chan() Chan

func (*EndNode) Child

func (e *EndNode) Child(i int) Node

func (*EndNode) Children

func (e *EndNode) Children() []Node

func (*EndNode) Kind

func (e *EndNode) Kind() op

func (*EndNode) String

func (e *EndNode) String() string

type GotoNode

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

GotoNode represents a jump (edge to existing LabelNode)

func (*GotoNode) Append

func (g *GotoNode) Append(n Node) Node

func (*GotoNode) Child

func (g *GotoNode) Child(i int) Node

func (*GotoNode) Children

func (g *GotoNode) Children() []Node

func (*GotoNode) Kind

func (g *GotoNode) Kind() op

func (*GotoNode) Name

func (g *GotoNode) Name() string

func (*GotoNode) String

func (g *GotoNode) String() string

type GraphvizDot

type GraphvizDot struct {
	Graph      *gographviz.Escape
	Count      int
	LabelNodes map[string]string
}

GraphvizDot reprents a new graphviz dot graph.

func NewGraphvizDot

func NewGraphvizDot(s *Session) *GraphvizDot

NewGraphvizDot creates a new graphviz dot graph from a session.

func (*GraphvizDot) WriteTo

func (dot *GraphvizDot) WriteTo(w io.Writer) (int64, error)

WriteTo implements io.WriterTo interface.

type LabelNode

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

LabelNode makes a placeholder for loop/jumping

func (*LabelNode) Append

func (l *LabelNode) Append(n Node) Node

func (*LabelNode) Child

func (l *LabelNode) Child(i int) Node

func (*LabelNode) Children

func (l *LabelNode) Children() []Node

func (*LabelNode) Kind

func (l *LabelNode) Kind() op

func (*LabelNode) Name

func (l *LabelNode) Name() string

func (*LabelNode) String

func (l *LabelNode) String() string

type NewChanNode

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

NewChanNode represents creation of new channel

func (*NewChanNode) Append

func (nc *NewChanNode) Append(n Node) Node

func (*NewChanNode) Chan

func (nc *NewChanNode) Chan() Chan

func (*NewChanNode) Child

func (nc *NewChanNode) Child(i int) Node

func (*NewChanNode) Children

func (nc *NewChanNode) Children() []Node

func (*NewChanNode) Kind

func (nc *NewChanNode) Kind() op

func (*NewChanNode) String

func (nc *NewChanNode) String() string

type Node

type Node interface {
	Kind() op               // For checking type without type switching
	Child(index int) Node   // Gets child at index
	Append(child Node) Node // Returns new child for chaining
	Children() []Node       // Returns whole slice
	String() string
}

A Node in the session graph.

func NewEndNode

func NewEndNode(ch Chan) Node

NewEndNode makse an EndNode.

func NewGotoNode

func NewGotoNode(name string) Node

NewGotoNode makes a GotoNode.

func NewLabelNode

func NewLabelNode(name string) Node

NewLabelNode makes a LabelNode.

func NewNewChanNode

func NewNewChanNode(ch Chan) Node

NewNewChanNode makes a NewChanNode.

func NewRecvNode

func NewRecvNode(orig Chan, rcvr Role, typ types.Type) Node

NewRecvNode makes a RecvNode.

func NewRecvStopNode

func NewRecvStopNode(orig Chan, rcvr Role, typ types.Type) Node

NewRecvStopNode makes a RecvNode (for STOP messages).

func NewSelectRecvNode

func NewSelectRecvNode(orig Chan, rcvr Role, typ types.Type) Node

NewSelectRecvNode makes a RecvNode in a select (non-deterministic).

func NewSelectSendNode

func NewSelectSendNode(sndr Role, dest Chan, typ types.Type) Node

NewSelectSendNode makes a SendNode in a select (non-deterministic).

func NewSendNode

func NewSendNode(sndr Role, dest Chan, typ types.Type) Node

NewSendNode makes a SendNode.

type NodeStack

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

NodeStack is a stack for sesstype.Node

func NewNodeStack

func NewNodeStack() *NodeStack

NewNodeStack returns a new NodeStack instance.

func (*NodeStack) Pop

func (s *NodeStack) Pop()

Pop removes a sesstype.Node from the stack.

func (*NodeStack) Push

func (s *NodeStack) Push(node Node)

Push pushes a sesstype.Node to the stack.

func (*NodeStack) Size

func (s *NodeStack) Size() int

Size returns number of sesstype.Node on the stack.

func (*NodeStack) String

func (s *NodeStack) String() string

String returns a String representing the stack.

func (*NodeStack) Top

func (s *NodeStack) Top() Node

Top returns the sesstype.Node at the top of the stack.

type RecvNode

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

RecvNode represents a receive.

func (*RecvNode) Append

func (r *RecvNode) Append(node Node) Node

func (*RecvNode) Child

func (r *RecvNode) Child(index int) Node

func (*RecvNode) Children

func (r *RecvNode) Children() []Node

func (*RecvNode) From

func (r *RecvNode) From() Chan

func (*RecvNode) IsNondet

func (r *RecvNode) IsNondet() bool

func (*RecvNode) Kind

func (r *RecvNode) Kind() op

func (*RecvNode) Receiver

func (r *RecvNode) Receiver() Role

func (*RecvNode) Stop

func (r *RecvNode) Stop() bool

func (*RecvNode) String

func (r *RecvNode) String() string

type Role

type Role interface {
	Name() string
}

Role in a session (main or goroutine).

type SendNode

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

SendNode represents a send.

func (*SendNode) Append

func (s *SendNode) Append(n Node) Node

func (*SendNode) Child

func (s *SendNode) Child(i int) Node

func (*SendNode) Children

func (s *SendNode) Children() []Node

func (*SendNode) IsNondet

func (s *SendNode) IsNondet() bool

func (*SendNode) Kind

func (s *SendNode) Kind() op

func (*SendNode) Sender

func (s *SendNode) Sender() Role

func (*SendNode) String

func (s *SendNode) String() string

func (*SendNode) To

func (s *SendNode) To() Chan

type Session

type Session struct {
	Types map[Role]Node              // Root Node for each Role
	Chans map[*utils.Definition]Chan // Actual channels are stored here
	Roles map[string]Role            // Actual roles are stored here
}

Session is a container of session graph nodes, also holds information about channels and roles in the current session.

func CreateSession

func CreateSession() *Session

CreateSession initialises a new empty Session.

func (*Session) GetRole

func (s *Session) GetRole(name string) Role

GetRole returns or create (if empty) a new session role using given name.

func (*Session) MakeChan

func (s *Session) MakeChan(v *utils.Definition, r Role) Chan

MakeChan creates and stores a new session channel created.

func (*Session) MakeExtChan

func (s *Session) MakeExtChan(v *utils.Definition, r Role) Chan

MakeExtChan creates and stores a new channel and mark as externally created.

func (*Session) String

func (s *Session) String() string

String displays session details.

Jump to

Keyboard shortcuts

? : This menu
/ : Search site
f or F : Jump to