sig
type expression =
PVar of string
| PPrm of string * string
| PCst of Logic_ptree.constant
| PBinop of Logic_ptree.binop * Promelaast.expression *
Promelaast.expression
| PUnop of Logic_ptree.unop * Promelaast.expression
| PArrget of Promelaast.expression * Promelaast.expression
| PField of Promelaast.expression * string
| PArrow of Promelaast.expression * string
type condition =
PRel of Logic_ptree.relation * Promelaast.expression *
Promelaast.expression
| PTrue
| PFalse
| POr of Promelaast.condition * Promelaast.condition
| PAnd of Promelaast.condition * Promelaast.condition
| PNot of Promelaast.condition
| PCall of string * string option
| PReturn of string
and seq_elt = {
condition : Promelaast.condition option;
nested : Promelaast.sequence;
min_rep : Promelaast.expression option;
max_rep : Promelaast.expression option;
}
and sequence = Promelaast.seq_elt list
type parsed_condition = Seq of Promelaast.sequence | Otherwise
type typed_condition =
TOr of Promelaast.typed_condition * Promelaast.typed_condition
| TAnd of Promelaast.typed_condition * Promelaast.typed_condition
| TNot of Promelaast.typed_condition
| TCall of Cil_types.kernel_function * Cil_types.funbehavior option
| TReturn of Cil_types.kernel_function
| TTrue
| TFalse
| TRel of Cil_types.relation * Cil_types.term * Cil_types.term
type single_action =
Counter_init of Cil_types.term_lval
| Counter_incr of Cil_types.term_lval
| Pebble_init of Cil_types.logic_info * Cil_types.logic_var *
Cil_types.logic_var
| Pebble_move of Cil_types.logic_info * Cil_types.logic_var *
Cil_types.logic_info * Cil_types.logic_var
| Copy_value of Cil_types.term_lval * Cil_types.term
type action = Promelaast.single_action list
type state = {
name : string;
mutable acceptation : Bool3.t;
mutable init : Bool3.t;
mutable nums : int;
mutable multi_state : (Cil_types.logic_info * Cil_types.logic_var) option;
}
type 'condition trans = {
start : Promelaast.state;
stop : Promelaast.state;
mutable cross : 'condition;
mutable numt : int;
}
type 'condition automaton =
Promelaast.state list * 'condition Promelaast.trans list
type parsed_automaton = Promelaast.parsed_condition Promelaast.automaton
type typed_automaton =
(Promelaast.typed_condition * Promelaast.action) Promelaast.automaton
type funcStatus = Call | Return
end