Logic Package

 

The logic package is used to represent formulas that can be verified by Cismo. In order to avoid any ambiguities in the formulas, every sub formulas must be delimited by parenthesis. The formula parser is able to recognize these elements:

 

True

Defines the true clause. Every state is true, therefore, when evaluating a true clause, the entire state space is returned.

Logical and

The and logical operator intersects the two state set returned by the linked sub formulas.

Logical or

The or logical operator unify the two state set returned by the linked sub formulas.

Logical not

The not logical operator negates the state set returned by the subformulas. The state set returned is a substraction of the sub formula state set from the entire state space.

Atomic proposition

Returns all the intervals linked to the specific atomic proposition.

Probabilistic next

Defines a probabilistic expression to evaluate. A probabilistic next expression contains at least an expression in the form <action>[probability] which returns all the states that can be reached with a probability of at least probability using the action action.

 

Formula :

The formula class represents a formula recognizable by Cismo. It is in fact a binary tree containing all the expressions included in the formula. A formula object cannot be instanced since formula is an abstract class. All six possible expression type implementing the formula interface can be followed by one or two subformulas. Computation of a formula is done recursively.

 

For example, the formula (<action4>[0.0]T)AND(<action2>[0.0]<action4>[0.0]T))OR((<action1>[0.0]T)OR(<action3>[0.2]T)) can be represented by this tree.

 

 

A valid formula must respect these restrictions:

1.      All leaves must be true clauses in order for the formula to be computable.

2.      A logical AND or a logical OR must link two subformulas (i.e. have two children).

3.      A logical NOT negates one subformula (only one child).

4.      A probabilistic next expression must use a valid action and have a probability included in the following interval [0,1[, it cannot be exactly one.

5.      The parenthesis must be balanced in order to build the formula tree.

 

LogicalParser :

 

Creating a formula using a tree would be difficult and would not be easily written into a file anyway. The role of the logical parser is to transform a regular string expression, with parenthesis to define the expression’s depth. The logical parser then converts the string into a formula tree, throwing an exception if an invalid construction is represented by the string. Any formula loaded from the disk, or built using the formula editor is converted into a string to be put in the formula history of Cismo. When a verification is requested, the string is reconverted into the formula tree so the verification can begin.

 

Data package, Generator package, Engine Trace,  Logic Package, Engine