This module implements functions for checking (bi)simulation relations of labeled transition systems (Kripke structures). It also computes quotients and products of Kripke structures.
Type | Description |
Function or value | Description |
|
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 ParseKripkeStructure, and then the various simulation and bisimulation relations are computed in addition to the quotient structures to minimize the given Kripke structures.
|
Full Usage:
CheckBisimulation ostr prefix1 K1 prefix2 K2
Parameters:
TextWriter
prefix1 : string
K1 : KripkeStructure
prefix2 : string
K2 : KripkeStructure
Returns: bool * (int * int) list
|
|
Full Usage:
CheckSimulation ostr prefix1 K1 prefix2 K2
Parameters:
TextWriter
prefix1 : string
K1 : KripkeStructure
prefix2 : string
K2 : KripkeStructure
Returns: bool * (int * int) list
|
|
|
Check whether each state has a unique label (this is required for making a symbolic representation of the Kripke structure).
|
Full Usage:
ComputeProduct k1 k2
Parameters:
KripkeStructure
k2 : KripkeStructure
Returns: KripkeStructure
|
|
Full Usage:
ComputeQuotient k sigma
Parameters:
KripkeStructure
sigma : (int * int) list
Returns: KripkeStructure
|
compute a quotient structure by a given equivalence relation; the states are those states of an equivalence class with minimal index
|
Full Usage:
Kripke2Dot ostr statePrefix k
Parameters:
TextWriter
statePrefix : string
k : KripkeStructure
|
|
Full Usage:
MkInitialRel k1 k2
Parameters:
KripkeStructure
k2 : KripkeStructure
Returns: (int * int) list
|
|
|
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;
|
Full Usage:
StateSet2String statePrefix s
Parameters:
string
s : Set<int>
Returns: string
|
|
|
|
Full Usage:
printSimDiagrams ostr prefix1 k1 prefix2 k2
Parameters:
TextWriter
prefix1 : string
k1 : KripkeStructure
prefix2 : string
k2 : KripkeStructure
|
|