Data package

ActInialPair : The class represents an association table between an action and all of the starting states from which it can be applied. The X state set is recomposed by adding all starting states from every action, and removing duplicates. Obtaining the X set is more time consuming because it cannot be directly accessed. On the other hand, the most frequently used operation is to obtain all the states from which an action can be applied, so this structure is more appropriate, because the latter can be computed with an efficiency of Θ(1), since all the values are stored using an hashing table.

ActInitialEndingTriplet : The class represents an association table between a couple formed by an action and its starting state set, with an associated ending state set. The Y set is recomposed by adding all the states from every couple, and removing duplicates. Again, use of this method is motivated by the fact it optimizes closure operations. This class also uses an hashing table to find the corresponding ending interval set. The ending sate set associated to a couple can be obtained with an efficiency of Θ(1).

Interval : Represents a set containing an uncountable number of different states. Both lower and upper bound, and their inclusion value (boolean) must be specified. If an interval has two equal bounds, then they must be both included, and they represent a discrete interval. Such interval only contain one state. An interval can be intersected our united with another one.

IntervalList : Contains a list of disjoints intervals. If an interval that intersects with a member of the list is added, then it is automatically unified. Intersection and unification of two list are possible. Two intervals are also unified should they be contiguous.

ProbSystem : Contains the probabilistic system to verify. A probabilistic system contains an initial state, a state space, a set of starting states, a set of ending states, actions that can be applied, atomic propositions which identify states to specific labels and a set of transitions.
The transitions have an initial state set x, an ending state set y, an action which must be applied, and an expression representing the probability of reaching a certain y state from a certain x state.

ProbSystemHash : Implementation of a probabilistic system using structures with hashing tables. This system is optimized for speed.

ProbSystemMTBDD : Implementation of a probabilistic system using multiterminal binary decision diagrams (MTBDD) for saving memory. Usually, a model checker fails by memory starving, so the usage of MTBDDs should enable verification of larger systems.

StandardNormalTable : Access a table containing standard reduced centered normal law distribution function values.

Transition : Represents a transitio in the system. A transition has the following parameters :
action : the action that is applied
startingStates : the set containing all the possible starting states for this transtion
endingStates : the se containing all the possible ending states for this transition
expression : contains an expression recognized by JavaMath to compute the probability to reach a y state from a x state.

Engine package, Generator package, Logic Package, Engine trace