sesstype

package
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: 1

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.

Source Files

View all Source files

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.