module Promelaast:sig
..end
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 |
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_init(set,aux,count) indicates that
pebble count is put in set whose content is governed by C
variable aux . | *) |
| |
Pebble_move of |
(* | 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 |
(* |
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
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
| *) |
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
| *) |
type'condition
automaton =state list * 'condition trans list
typeparsed_automaton =
parsed_condition automaton
typetyped_automaton =
(typed_condition * action) automaton
type
funcStatus =
| |
Call |
| |
Return |