How does it work ?

The Engine package :

First, it is important to understand how the system is stored in memory. Unlike in a lmp file, the starting state set X and editing state set Y are not stored directly in memory. Instead, all the system using three data structures :

pairs :  action -> initial state set
The idea behind this data structure is to be able to quickly obtain all the states for which the action may be applied. The separe function use this list extensively to obtain all the starting states. The advantage of using this method is that all starting states for an action may be obtain with an efficiency of Θ(1). One major disadvantage is that the X array is never directly accessible in memory. In order to obtain it, all starting state for every action must be added, while eliminating duplicates, with an efficiency of Ω(n). Since the latter is not used as often, this is acceptable.

triplets : (action, initial state) -> ending state
In order to obtain the ending state, a pair must be formed first. When evaluating a formula, this map is very efficient, enabling the engine to quickly obtain the Cartesian product of starting states for action X ending states. One major drawback of this method is that the Y state set is not directly accessible and must be recomposed, just like the X state set, eliminating duplicates. When dealing with an almost connected LMP system (almost every ending state has a transition for every starting state), this generation can be time consuming.

quads : (action, initial state, ending state) -> transition
Returns the transition object associated with the three parameters. This enables to obtain a transition with an efficiency of Θ(1), which would not be possible if seeking the transition in the list. The triplet formed by the three parameters is hashed to directly obtain the associated transition.

Engine.findZeroes : This method returns all the states from the specified set using the specified expression to compute the probabilities. In order to find the zeroes, the function split the original interval into segmentation number intervals. Then the function analyse the sign of the function (positive if ascending, negative if descending). When the interval within two bounds with opposed signs is found, the interval is split again by calling findZeroes recursively. When iterations calls have been made, the point is calculated using the secant method. The higher segmentation and iterations, the zeroes will be more accurate, at the expense of performance.

Engine.separe : This function returns an interval list representing all the x from the original interval list (provided upon function call) for which the probability to each a least one y is at least q (provided upon function call). To compute this, the function first call findZeroes which will find all points within a probabilistic function that intersect with q. Then the function checks if the function is ascending after the zero. To compute this, a point is chosen between two zeroes, and if this point is greater than q, then the function is ascending.

Engine.getAllStatesVerifying : The formula tree analysis is done recursively. Each subexpression is then analysed as follow :
- a true clause returns all of the state space
- a NOT operator returns the state space minus all the states returned by the following subexpression
- an OR logical operator returns the union of its two linked subexpressions
- an AND logical operator returns the intersection of its two linked subexpression
- if a probabilistic expression in the form of <action>[probability] is found, then the separe function is called with all the starting intervals which are linked to the action as parameter, and probability as q.

Engine.loadFormula (File) : This function is a replacement for the standard lmp file loader. Instead of fetching the system from a file, a large string object is used instead. Used in conjunction of saveFormula(File), it can be used to rebuild the system from MTBDDs data structure to standard hash based sructures.

Also see :
Data package, Generator package, Logic Package, Engine trace