Formula Editor
The formula editor is a coloured syntax editor. The wizard is divided into three main regions :
1. The operators section includiding the operators AND, OR, NOT and a probabilistic expression in the format <action>[maximum probability]. The parenthesis are green, the logical operators in pink, the true clauses in red and the probabilistic expressions in blue.
2. The formula line containing the formula, in which we may move the cursor using the two arrows, or edit the formula directly using the keyboard.
3. The commands that can be executed from the formula editor :
| Check initial state | Verify that the initial states verifies the current formula. |
| Get all states verifying the formula | Get the state set that verifies this formula on the currently loaded system. |
| Verify formula syntax | Check the validity of the formula but does not verify the system. |
| Cancel | Returns to Cismo discarding changes. |
The formulas must respect the following constraints :
1. Every subformula must be enclosed between parenthesis and must end with a true clause.
2. A logical operator AND or OR must link two subformulas.
3. A formula must contain at least one true clause.
4. The parenthesis balance must be null (same number of left and right parenthesis).
5. The negator NOT, must be placed between a subformula.
Once the formula has been input, you way check its syntax by clicking on the "verify formua syntax" button. If the formula is not valid, you will receive a message box explaining the problem. Otherwise, you will receive a confirmation dialog with an additionnal option : view the graphical representation of the formula. Basically, this is the formula transformed into a tree.
For example, this is the graphical representation of
((<action4>[0.0]T)AND(<action2>[0.0]<action4>[0.0]T))OR((<action1>[0.0]T)OR(<action3>[0.2]T)).
Note that if an invalid keyword is detected in the formula, it will appear in
gray italic.
States verifying the formula
If you clicked the "check initial state", you will receive a message specifying wether or not the formula can be validated by the initial state. If you clicked the "get states verifying formula", you will get all the states that verify the formula. For example :
Notice the "show trace" button. This is very useful to analyse the answer given to you by Cismo, especially if the answer is that no state satisfies the formula. The formula trace should look like this :
There are three panes, corresponding to three type of trace :
Trace by occurence in the formula :
The evaluations are printed in the same order you actually read the formula. However, if a lot of parenthesis are present, this may become very confusing.
Trace by order of evaluation :
The evaluations are printed in their order of evaluation. If your formula contains a lot of parenthesis, you should select this mode.
Tree view :
This is by far the most useful representation of the formula evaluation. However, the tree may become very large and impossible to send to the printer.