transforms

Documentation

Overview

Package transforms declares the types and functions used to transform and work with some type of FSA. Come of the transformation implemented here are standard such as determinization (Subset Construction), minimization but more are specifically related to Choreia (GoroutineFSA extraction & Composition)

Package transforms declares the types and functions used to transform and work with some type of FSA. Come of the transformation implemented here are standard such as determinization (Subset Construction), minimization but more are specifically related to Choreia (GoroutineFSA extraction & Composition)

Package transforms declares the types and functions used to transform and work with some type of FSA. Come of the transformation implemented here are standard such as determinization (Subset Construction), minimization but more are specifically related to Choreia (GoroutineFSA extraction & Composition)

Index

• func ExtractGoroutineFSA(file meta.FileMetadata) map[string]*GoroutineFSA
• func LocalViewsComposition(localViews map[string]*GoroutineFSA) *fsa.FSA
• func SubsetConstruction(NCA *fsa.FSA) *fsa.FSA
• type FrozenFSA
• type GoroutineFSA
• type ProductFSA

Functions

func ExtractGoroutineFSA

func ExtractGoroutineFSA(file meta.FileMetadata) map[string]*GoroutineFSA

Given the metadata associated to a file it linearizes the automata found in it (function calls inlining). Once done that extracts recursively the FSA associated to each Goroutine spawned during the program execution, the latter are returned as output

func LocalViewsComposition

func LocalViewsComposition(localViews map[string]*GoroutineFSA) *fsa.FSA

Takes the deterministic version of the Local Views (or Projection Automata) and merges them in one DCA that will represent the choreography as a whole (the global view). This is possible by composing all the Local View's FSAs into one and then appply a Synchronization transform on it

func SubsetConstruction

func SubsetConstruction(NCA *fsa.FSA) *fsa.FSA

An adapted version of the classic Subset Construction Algorithm for FSA determinization. Allows to transform a Nondeterministic Finite State Automaton (NFA) to an equivalent Deterministic Finite State Automaton (DFA), the latter doesn't present eps-transition or duplicated parallel labels and its easier to be understood by humans

Types

type FrozenFSA

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

A struct representing a "frozen" state of an FSA

type GoroutineFSA

type GoroutineFSA struct {
	Name string // An identifier for the Automata
	meta.FuncMetadata
}

A FSA that represents the execution flow of a single Goroutine (identified by its own name) this will be used in the future phases as a local view for the whole choreography. This means that this FSA will provide an "isolated" view of the choreography from the perspective of the Goroutine that takes part in it (almost like a projection of the whole choreography)

type ProductFSA

type ProductFSA *list.List // A list of (FrozenAutomata, FrozenAutomata) tuples