KripkeStructures (Averest) | Averest

KripkeStructures Module

Namespace: Averest.TeachingTools
Assembly: Averest.dll

This module implements functions for checking (bi)simulation relations of labeled transition systems (Kripke structures). It also computes quotients and products of Kripke structures.

Types

Type	Description
KripkeStructureExpl	This denotes the type of a Kripke structure. States are unsigned integers, and the labels are then given by a simple array of sets of strings, and the transition relation is a list of pairs of states (integers). Finally,the initial states are given as a set of states.

Functions and values

Function or value	Description
`BisimulationQuotientsTool qscoll` Full Usage: `BisimulationQuotientsTool qscoll` Parameters: qscoll : `NameValueCollection`	This function is meant to be called from cgi; it expects two Kripke structures given as name value pairs in the qscoll argument where the names are Kripke1 and Kripke2. The values are parsed by function ParseKripkeStructureExpl, and then the various simulation and bisimulation relations are computed in addition to the quotient structures to minimize the given Kripke structures. qscoll : `NameValueCollection`
`CheckBisimulation ostr prefix1 K1 prefix2 K2` Full Usage: `CheckBisimulation ostr prefix1 K1 prefix2 K2` Parameters: ostr : `TextWriter` prefix1 : `string` K1 : `KripkeStructureExpl` prefix2 : `string` K2 : `KripkeStructureExpl` Returns: `bool * Set<int * int>`	check whether K1 and K2 are bisimilar ostr : `TextWriter` prefix1 : `string` K1 : `KripkeStructureExpl` prefix2 : `string` K2 : `KripkeStructureExpl` Returns: `bool * Set<int * int>`
`CheckSimulation ostr prefix1 K1 prefix2 K2` Full Usage: `CheckSimulation ostr prefix1 K1 prefix2 K2` Parameters: ostr : `TextWriter` prefix1 : `string` K1 : `KripkeStructureExpl` prefix2 : `string` K2 : `KripkeStructureExpl` Returns: `bool * Set<int * int>`	check whether K2 simulates K1 ostr : `TextWriter` prefix1 : `string` K1 : `KripkeStructureExpl` prefix2 : `string` K2 : `KripkeStructureExpl` Returns: `bool * Set<int * int>`
`CheckUniqueLabels k` Full Usage: `CheckUniqueLabels k` Parameters: k : `KripkeStructureExpl` Returns: `bool`	Check whether each state has a unique label (this is required for making a symbolic representation of the Kripke structure). k : `KripkeStructureExpl` Returns: `bool`
`ComputeProduct k1 k2` Full Usage: `ComputeProduct k1 k2` Parameters: k1 : `KripkeStructureExpl` k2 : `KripkeStructureExpl` Returns: `KripkeStructureExpl`	compute a product structure of given Kripke structures k1 : `KripkeStructureExpl` k2 : `KripkeStructureExpl` Returns: `KripkeStructureExpl`
`ComputeQuotient k sigma` Full Usage: `ComputeQuotient k sigma` Parameters: k : `KripkeStructureExpl` sigma : `Set<int * int>` Returns: `KripkeStructureExpl`	compute a quotient structure by a given equivalence relation; the states are those states of an equivalence class with minimal index k : `KripkeStructureExpl` sigma : `Set<int * int>` Returns: `KripkeStructureExpl`
`Kripke2Dot ostr statePrefix k` Full Usage: `Kripke2Dot ostr statePrefix k` Parameters: ostr : `TextWriter` statePrefix : `string` k : `KripkeStructureExpl`	write Kripke structure to a dot file ostr : `TextWriter` statePrefix : `string` k : `KripkeStructureExpl`
`MkInitialRel k1 k2` Full Usage: `MkInitialRel k1 k2` Parameters: k1 : `KripkeStructureExpl` k2 : `KripkeStructureExpl` Returns: `Set<int * int>`	construct all pairs of states of the two structures having the same labels k1 : `KripkeStructureExpl` k2 : `KripkeStructureExpl` Returns: `Set<int * int>`
`ParseKripkeStructureExpl s` Full Usage: `ParseKripkeStructureExpl s` Parameters: s : `string` Returns: `KripkeStructureExpl`	parsing a Kripke structure from a string; the syntax is explained by the following example: vars a,b,c,d; init 0,1; labels 0:a,b; 1:b; 2:b,c; 3:c; 4:d; 5:c; transitions 0->1; 0->2; 1->3; 1->4; 2->5; 3->3; 4->4; 5->5; s : `string` Returns: `KripkeStructureExpl`
`StateSet2String statePrefix s` Full Usage: `StateSet2String statePrefix s` Parameters: statePrefix : `string` s : `Set<int>` Returns: `string`	statePrefix : `string` s : `Set<int>` Returns: `string`
`SymbolicPreSuccessorTool qscoll` Full Usage: `SymbolicPreSuccessorTool qscoll` Parameters: qscoll : `NameValueCollection`	This cgi-function is used to compute predecessor and successor states in a symbolic way by simply expanding the boolean quantifier into the disjunction/conjunction of the cofactors. qscoll : `NameValueCollection`
`mkSymbolicRepresentation k` Full Usage: `mkSymbolicRepresentation k` Parameters: k : `KripkeStructureExpl` Returns: `string`	generate a symbolic description of the Kripke structure in DNF k : `KripkeStructureExpl` Returns: `string`
`printSimDiagrams ostr prefix1 k1 prefix2 k2` Full Usage: `printSimDiagrams ostr prefix1 k1 prefix2 k2` Parameters: ostr : `TextWriter` prefix1 : `string` k1 : `KripkeStructureExpl` prefix2 : `string` k2 : `KripkeStructureExpl`	prints the diagrams for iterating the simulation relations ostr : `TextWriter` prefix1 : `string` k1 : `KripkeStructureExpl` prefix2 : `string` k2 : `KripkeStructureExpl`