Module Promelaast

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 string
| PPrm of string * string
| PCst of Logic_ptree.constant
| PBinop of Logic_ptree.binop * expression * expression
| PUnop of Logic_ptree.unop * expression
| PArrget of expression * expression
| PField of expression * string
| PArrow of expression * string
type condition = 
| PRel of Logic_ptree.relation * expression * expression
| PTrue
| PFalse
| POr of condition * condition
| PAnd of condition * condition
| PNot of condition
| PCall of string * string option (*

Call might be done in a given behavior

*)
| PReturn of string
type seq_elt = {
   condition : condition option;
   nested : sequence;
   min_rep : expression option;
   max_rep : expression option;
}
type sequence = seq_elt list 
type parsed_condition = 
| Seq of sequence
| 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 typed_condition * typed_condition (*

Logical OR

*)
| TAnd of typed_condition * typed_condition (*

Logical AND

*)
| TNot of typed_condition (*

Logical NOT

*)
| TCall of Cil_types.kernel_function * Cil_types.funbehavior option (*

Predicate modelling the call of an operation

*)
| TReturn of Cil_types.kernel_function (*

Predicate modelling the return of an operation

*)
| TTrue (*

Logical constant TRUE

*)
| TFalse (*

Logical constant FALSE

*)
| TRel of Cil_types.relation * Cil_types.term * Cil_types.term (*

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 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 (*

adds a new pebble. Pebble_init(set,aux,count) indicates that pebble count is put in set whose content is governed by C variable aux.

*)
| Pebble_move of Cil_types.logic_info * Cil_types.logic_var * Cil_types.logic_info
* Cil_types.logic_var
(*

Pebble_move(new_set,new_aux,old_set,old_aux) moves pebbles from old_set to new_set, governed by the corresponding aux variables.

*)
| Copy_value of Cil_types.term_lval * Cil_types.term (*

copy the current value of the given term into the given location so that it can be accessed by a later state.

*)
type action = 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 : string; (*

State name

*)
   mutable acceptation : Bool3.t; (*

True iff state is an acceptation state

*)
   mutable init : Bool3.t; (*

True iff state is an initial state

*)
   mutable nums : int; (*

Numerical ID of the state

*)
   mutable multi_state : (Cil_types.logic_info * Cil_types.logic_var) option; (*

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 : state; (*

Starting state of the transition

*)
   stop : state; (*

Ending state of the transition

*)
   mutable cross : 'condition; (*

Cross condition of the transition

*)
   mutable numt : int; (*

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.

type parsed_automaton = parsed_condition automaton 
type typed_automaton = (typed_condition * action) automaton 
type funcStatus = 
| Call
| Return

An operation can have two status: currently calling or returning.