Mefresa.Behaviour.LTS
In this module we define the LTS datatype. Its mechanization
is rather familiar with the classifical definition
of labelled transition systems. Further, we show how to
encode the notion of execution traces.
Require Export String.
Require Export List.
Require Export Mefresa.Batteries.
Require Export Mefresa.Behaviour.LTL.
Notation " [ ] " := nil : list_scope.
Notation " [ x ] " := (cons x nil) : list_scope.
Notation " [ x ; .. ; y ] " := (cons x .. (cons y nil) ..) : list_scope.
LTS datatype
Definition state_mem : Type := list (string * nat) .
Inductive lts_state :=
| LTS_State : nat -> state_mem -> lts_state.
We go for a rather simple notion of lts_state. They are
identified by a natural number. Further, they possess a memory,
state_mem, that is a simple mapping between strings and nats.
Function beq_lts_state q q' : bool :=
match q, q' with
LTS_State n mem, LTS_State n' mem' => beq_nat n n'
end.
Notation "q1 '===' q2" := (beq_lts_state q1 q2) (at level 5, left associativity).
Function update_lts_state_mem q mem : lts_state :=
match q with
LTS_State n _ => LTS_State n mem
end.
Notation "mem '->>' q" := (update_lts_state_mem q mem) (at level 4, left associativity).
Comparing and updating lts_states is rather trivial. Comparison
boils down to comparing natural numbers. We do not compare the contents
of their memory as we usually simply want to check their identifier.
Updating a lts_state simply means replacing its state_mem
field.
Definition lts_states := list lts_state.
Inductive communication_type : Type :=
| Read: communication_type
| Emit: communication_type.
Function beq_comm_type ct1 ct2 : bool :=
match ct1, ct2 with
Read, Read => true
| Emit, Emit => true
| _, _ => false
end.
Inductive parameter : Type :=
Val : nat -> parameter
| Var : string -> parameter.
Definition parameters := list parameter.
Function beq_parameter p1 p2 : bool :=
match p1, p2 with
Val n, Val n' => beq_nat n n'
| Var s, Var s' => beq_string s s'
| _, _ => false
end.
Inductive message : Type :=
| Message: string -> communication_type -> parameters -> message.
Inductive assignment :=
| Assignment : string -> nat -> assignment
| AssignmentVar: string -> string -> assignment. Notation "'[' value '\' var ']'" := (Assignment var value).
Notation "'[' varY '/' varX ']'" := (AssignmentVar varX varY).
Definition assignments : Type := list assignment.
Inductive action : Type :=
Action : message -> assignments -> action.
Another rather standard element of LTSs are actions. These
are constituted by a message and assignments. A message
holds a string as its label, a communication_type and
parameters. assignments simply indicate what variable
needs to be set.
Definition actions := list action.
Definition transitions := list(lts_state * action * lts_state).
Record LTS : Type := mk_LTS
{ States : lts_states ;
Init : lts_state ;
Actions : actions ;
Transitions : transitions
}.
Finally, the LTS datatype is defined by adequately composing the
already seen lts_state and action datatypes.
Let us now see how we can define traces for the LTS datatype.
Traces for LTS
Fixpoint beq_message m1 m2 : bool :=
match m1, m2 with
Message l ct ps, Message l' ct' ps' => beq_string l l' && beq_comm_type ct ct' &&
(fix beq_parameters lp lp' :=
match lp, lp' with
nil, nil => true
| p :: r, p'::r' => beq_parameter p p' && beq_parameters r r'
| _, _ => false
end
) ps ps'
end.
Function valuation (v:string) (mem:state_mem) : nat :=
match mem with
nil => 0
| (var, val) :: r => if beq_string var v then
val
else
valuation v r
end.
Fixpoint process_assignment (mem:state_mem) asgn : state_mem :=
match asgn with
Assignment v va =>
(fix fix_process_assignment mem :=
match mem with
nil => nil
| (var, val) :: r => if beq_string v var then
(var, va) :: process_assignment r asgn
else
(var, val) :: process_assignment r asgn
end
) mem
| AssignmentVar v varY =>
let va := valuation varY mem in
(fix fix_process_assignment mem :=
match mem with
nil => nil
| (var, val) :: r => if beq_string v var then
(var, va) :: process_assignment r asgn
else
(var, val) :: process_assignment r asgn
end
) mem
end.
Function process_assignments (mem:state_mem) asgns : state_mem :=
match asgns with
nil => nil
| asgn :: r => let mem' := process_assignment mem asgn in
process_assignments mem' r
end.
Function lts_get_target_state (ts:transitions)
(st:lts_state) (m:message) : option lts_state :=
match ts with
nil => None
| (q, Action me asgn, qs) :: r =>
if st === q && beq_message me m then
match st with
LTS_State _ q_mem =>
let q_mem_upd := process_assignments q_mem asgn in
Some (q_mem_upd->>qs)
end
else
lts_get_target_state r st m
end.
Definition lts_target_state (A:LTS) (st:lts_state) (m:message) : option lts_state :=
match m with
Message "-" _ _ => Some st
| _ => lts_get_target_state (@Transitions A) st m
end.
The function lts_target_state is one of the most important
definitions regarding the LTS datatype. Basically, it computes
the attained lts_state from the current lts_state,
by the given message.
CoInductive LTS_Trace (A:LTS) : lts_state -> LList (action) -> Prop :=
| lts_empty_trace : forall (m:message) (asgns:assignments) (q:lts_state),
In (Action m asgns) (@Actions A) ->
(lts_target_state A q m = None) ->
LTS_Trace A q LNil
| lts_lcons_trace : forall (q q':lts_state)
(m:message) (asgns:assignments) (l:LList (action)),
In (Action m asgns) (@Actions A) ->
Some q' = (lts_target_state A q m) ->
LTS_Trace A q' l ->
LTS_Trace A q (LCons (Action m asgns) l).
The LTS_Trace predicate is defined co-inductively as we
potentially deal with infinite traces. It possesses two constructors,
one for a deadlock situation, and another when proceeding execution.
Function lts_allowed_actions (q:lts_state) (ts:transitions) : actions :=
match ts with
nil => nil
| (qi, Action me asgn, qf) :: r => if q === qi then
(Action me asgn) :: lts_allowed_actions q r
else
lts_allowed_actions q r
end.
The above function returns the list of actions that can occur
from lts_state. It shall be useful at a later stage.