|
||||||||||
PREV CLASS NEXT CLASS | FRAMES NO FRAMES | |||||||||
SUMMARY: NESTED | FIELD | CONSTR | METHOD | DETAIL: FIELD | CONSTR | METHOD |
java.lang.Objectca.mcgill.lmp.finite.Bisim
Bisim encapsulates all the information required to run the bisim() algorithm. It
also contains the method getLumpedLMP() that build a lumped LMP using the
information produced by bisim(). A common usage would be:
Bisim bisim = new Bisim(myLMP);
bisim.bisim();
LMP lumpedLMP = bisim.getLumpedLMP;
System.out.println("result: " + lumpedLMP.toString();
Constructor Summary | |
Bisim(LMP lmp)
Create an instance of LMP to lump the given lmp. |
Method Summary | |
void |
bisim()
This algorithm allows us to distinguish states that do not satisfy the same formulas in the following logic:
L0 :== T | f_1 ^ f_2 | q f
This logic has the property to characterize bisimulation: two states are
bisimilar iff they satisfy the same formulas in L0. |
java.util.Set |
getD1()
See bisim(). |
java.util.Map |
getFormulas()
A way to obtain the formulas as a map indexed by the sets of D1 and mapped to the formula in L0 (a String) that all the states in the given set satisfy. |
LMP |
getLumpedLMP()
After the execution of bisim(), Bisim has all the infomation required to compute a simplified, "lumped" LMP. |
static void |
main(java.lang.String[] args)
bisim [optionalArguments] <inputFile>
Bisim takes the description of a LMP as input and outputs a LMP obtained by quotienting the input LMP by the equivalence relation of bisimulation First argument: the path to a file describing a LMP Optional arguments: --transitions Output the transition matrices of the new LMP --sets Output the set D1 used in an intermediate step The LMP should be described using the following specification: The description should be a list of transition matrices (one per label) separated by the "\n*\n" string. |
static void |
printUsage()
Print in System.err a description of the functionalities of main(). |
Methods inherited from class java.lang.Object |
equals, getClass, hashCode, notify, notifyAll, toString, wait, wait, wait |
Constructor Detail |
public Bisim(LMP lmp)
lmp
- Method Detail |
public void bisim()
L0 :== T | f_1 ^ f_2 | q f
This logic has the property to characterize bisimulation: two states are
bisimilar iff they satisfy the same formulas in L0.
Beginning with D1 containing only the set of all states, bisim operates as
follow: for each label a in the set of labels and B2 in D1, it ``splits''
every set B1 of D1 into subsets having the same probability of jumping to B2
with action a; this is done until it does not modify D1. At the end, all
states satisfying the same formulas will belong to exactly the same sets in
D1.
public java.util.Set getD1()
public java.util.Map getFormulas()
public LMP getLumpedLMP()
public static void main(java.lang.String[] args)
bisim [optionalArguments] <inputFile>
args
- public static void printUsage()
|
||||||||||
PREV CLASS NEXT CLASS | FRAMES NO FRAMES | |||||||||
SUMMARY: NESTED | FIELD | CONSTR | METHOD | DETAIL: FIELD | CONSTR | METHOD |