module Promelaast:sig
..end
The abstract tree of promela representation. Such tree is used by promela parser/lexer before its translation into Data_for_aorai module.
type
expression =
| |
PVar of |
| |
PPrm of |
| |
PCst of |
| |
PBinop of |
| |
PUnop of |
| |
PArrget of |
| |
PField of |
| |
PArrow of |
type
condition =
| |
PRel of |
|||
| |
PTrue |
|||
| |
PFalse |
|||
| |
POr of |
|||
| |
PAnd of |
|||
| |
PNot of |
|||
| |
PCall of |
(* | Call might be done in a given behavior | *) |
| |
PReturn of |
type
seq_elt = {
|
condition : |
|
nested : |
|
min_rep : |
|
max_rep : |
typesequence =
seq_elt list
type
parsed_condition =
| |
Seq of |
| |
Otherwise |
Promela parsed abstract syntax trees. Either a sequence of event or the otherwise keyword. A single condition is expressed with a singleton having an empty nested sequence and min_rep and max_rep being equal to one.
type
typed_condition =
| |
TOr of |
(* | Logical OR | *) |
| |
TAnd of |
(* | Logical AND | *) |
| |
TNot of |
(* | Logical NOT | *) |
| |
TCall of |
(* | Predicate modelling the call of an operation | *) |
| |
TReturn of |
(* | Predicate modelling the return of an operation | *) |
| |
TTrue |
(* | Logical constant TRUE | *) |
| |
TFalse |
(* | Logical constant FALSE | *) |
| |
TRel of |
(* | Condition. If one of the terms contains TResult, TRel is in conjunction with exactly one TReturn event, and the TResult is tied to the corresponding value. | *) |
type
single_action =
| |
Counter_init of |
|||
| |
Counter_incr of |
|||
| |
Pebble_init of |
(* | adds a new pebble. | *) |
| |
Pebble_move of |
(* |
| *) |
| |
Copy_value of |
(* | copy the current value of the given term into the given location so that it can be accessed by a later state. | *) |
typeaction =
single_action list
Additional actions to perform when crossing a transition. There is at most one Pebble_* action for each transition, and each transition leading to a state with multi-state has such an action.
type
state = {
|
name : |
(* | State name | *) |
|
mutable acceptation : |
(* | True iff state is an acceptation state | *) |
|
mutable init : |
(* | True iff state is an initial state | *) |
|
mutable nums : |
(* | Numerical ID of the state | *) |
|
mutable multi_state : |
(* | Translation of some sequences might lead to some kind of pebble automaton, where we need to distinguish various branches. This is done by having a set of pebbles instead of just a zero/one switch to know if we are in the given state. The guards apply to each active pebble and are thus of the form \forall integer x; in(x,multi_state) ==> guard. multi_state is the first lvar of the pair, x is the second | *) |
Internal representation of a State from the Buchi automata.
type 'condition
trans = {
|
start : |
(* | Starting state of the transition | *) |
|
stop : |
(* | Ending state of the transition | *) |
|
mutable cross : |
(* | Cross condition of the transition | *) |
|
mutable numt : |
(* | Numerical ID of the transition | *) |
Internal representation of a transition from the Buchi automata.
type'condition
automaton =state list * 'condition trans list
Internal representation of a Buchi automata : a list of states and a list of transitions.
typeparsed_automaton =
parsed_condition automaton
typetyped_automaton =
(typed_condition * action) automaton
type
funcStatus =
| |
Call |
| |
Return |
An operation can have two status: currently calling or returning.