Mefresa.Behaviour.Net
In this module we define the Net datatype. Basically, it is made of
the already seend LTS datatype, and a new datatype, SynchronizationVector,
representing synchronization vectors.
Inductive SyncronizationElement : Type :=
| WildCard : SyncronizationElement
| SyncElement : string -> SyncronizationElement.
Inductive SyncronizationOutput : Type :=
| GlobalAction: string -> SyncronizationOutput.
Inductive SynchronizationVector :=
SyncVector: list SyncronizationElement * SyncronizationOutput -> SynchronizationVector.
Function get_sync_output sv : string :=
match sv with
SyncVector (_, (GlobalAction l)) => l
end.
Definition sync_notation (a:string) : SyncronizationElement :=
match a with
"-" => WildCard
| _ => SyncElement a
end.
Notation "<< A , .. , B >> -> C" := (SyncVector((cons (sync_notation A) .. (cons (sync_notation B) nil) .. ), GlobalAction C)) (at level 80, right associativity).
Above, we defined the SynchronizationVector along with a convenient and familiar notation.
Its understanding should pose no doubt. It is composed by a list of synchronization elements,
and a resulting output.
Having defined synchronization vectors, we can now proceed defining the Net datatype and
its associated state.
Net datatype
Inductive Net : Type :=
| mk_SingletonNet: LTS -> Net
| mk_Net : (list LTS * list SynchronizationVector) -> Net.
Inductive net_state : Type :=
| NetSingleton_State: lts_state -> net_state
| Net_State : list lts_state -> net_state.
A Net is either made of a single LTS, or by several, in which case it includes
synchronization vectors specifying how these communicate with each other.
Moreover, its associated net_state, is either made of one lts_state,
or several.
Having defined the core datatypes for Nets, we can now proceed with
the machaninery involving Net_Traces.
Traces for Nets
Function beq_message_label (m:message) (sve:SyncronizationElement) : bool :=
match m, sve with
Message l _ct _lp, WildCard => false
| Message l _ct _lp, SyncElement a => beq_string l a
end.
Function lts_allowed_actions_with_label
(q:lts_state) (ts:transitions) (sve:SyncronizationElement): actions :=
match ts with
nil => nil
| (qi, Action me asgn, qf) :: r => if q === qi && beq_message_label me sve then
(Action me asgn) :: lts_allowed_actions_with_label q r sve
else
lts_allowed_actions_with_label q r sve
end.
Definition stay_in_state : action := Action (Message "-" Read nil) nil.
Function get_allowed_acts_from_sve (lts_obj:LTS) (lts_state:lts_state)
(sve:SyncronizationElement) : list action :=
match sve with
WildCard => stay_in_state :: nil
| _ => lts_allowed_actions_with_label lts_state (@Transitions lts_obj) sve
end.
Function allowed_actions_from_sv_element list_lts lts_states sv_elements : list (list action) :=
match list_lts, lts_states, sv_elements with
nil , nil , nil => nil
| lts_obj :: r, lts_st :: r', sve :: r'' =>
let acts := get_allowed_acts_from_sve lts_obj lts_st sve in
acts :: (allowed_actions_from_sv_element r r' r'')
| _, _, _ => nil
end.
The above functions are responsible for computing the possible actions that
may occur at each LTS composing the system, w.r.t. current lts_state they
are in, and the activated synchronization vector.
Set Implicit Arguments.
Function combine_aux (X:Type) (e:X) (l:list X) : list (list X) :=
match l with
nil => nil
| a :: r => (e::a::nil) :: combine_aux e r
end.
Function combine (X:Type) (l1 l2:list X) : list (list X) :=
match l1 with
nil => nil
| a :: r => app (combine_aux a l2) (combine r l2)
end.
Function combine_l2_in_l1 (X:Type) (l1 l2:list X) : list (list X) :=
match l2 with
nil => nil
| e :: r => (app l1 [e]) :: combine_l2_in_l1 l1 r
end.
Function combine_l2_in_l1s (X:Type) (ll1:list (list X)) (l2:list X) : list (list X) :=
match ll1 with
nil => nil
| l1 :: r => let ll1' := combine_l2_in_l1 l1 l2 in
app ll1' (combine_l2_in_l1s r l2)
end.
Function combine_l2s_in_l1s_aux (X:Type) (ll1:list (list X))
(ll2:list (list X)) acc : list (list X) :=
match ll2 with
nil => acc
| l2 :: r => let ll1' := combine_l2_in_l1s ll1 l2 in
combine_l2s_in_l1s_aux ll1' r ll1'
end.
Function combine_l2s_in_l1s (X:Type) (ll1 ll2: list (list X)) :=
combine_l2s_in_l1s_aux ll1 ll2 nil.
Function combineN (X:Type) (ll: list (list X)) : list (list X) :=
match ll with
nil => nil
| l :: nil => l :: nil
| l1 :: l2 :: nil => combine l1 l2
| l1 :: l2 :: r => let ll := combine l1 l2 in
combine_l2s_in_l1s ll r
end.
The combineN function, along with its dependencies, will be useful for
generating the set of possible synchronized actions that may occur.
Function get_target_lts_states (lq: list lts_state) (list_lts: list LTS)
(acts:list action)
: (list (lts_state * (communication_type * parameters))) :=
match lq, list_lts, acts with
nil , nil , nil => nil
| q :: r, lts_obj :: r', Action me _a :: r'' =>
match lts_target_state lts_obj q me with
None => nil
| Some q' => match me with
Message _l ct lp => ((q', (ct, lp))) :: get_target_lts_states r r' r''
end
end
| _, _, _ => nil
end.
The function get_target_lts_states computes the list of attained lts_states, along
with information regarding the action that took place.
Function message_parameter_to_emit (list_st_msg : (list (lts_state * (communication_type * parameters)))) :=
match list_st_msg with
nil => nil
| (q, (ct, lp)) :: r => match ct with
Read => message_parameter_to_emit r
| Emit => lp
end
end.
Function pass_message (q_mem: state_mem) (lp la:parameters) : state_mem :=
match lp, la with
nil , nil => q_mem
| Val n :: r, Val m :: r' =>
pass_message q_mem r r'
| Var x :: r, Var y :: r' =>
pass_message q_mem r r'
| Var x :: r, Val n :: r' => let q_mem' := process_assignment q_mem [n \ x] in
pass_message q_mem' r r'
| _, _ => q_mem
end.
Function message_passing (q:lts_state) (lp la: parameters) : lts_state :=
match q with
LTS_State _ q_mem =>
let q_mem_upd := pass_message q_mem lp la in
(q_mem_upd->>q)
end.
Function transmit_message (la:parameters) (list_st_msg : (list (lts_state * (communication_type * parameters)))) :=
match list_st_msg with
nil => nil
| (q, (ct, lp)) :: r => match ct with
Read => let q' := message_passing q lp la in
q' :: transmit_message la r
| Emit => q :: transmit_message la r
end
end.
The function transmit_message takes care of all the machinery dealing with the
transmission of messages values.
Function global_action_output (svo:SyncronizationOutput) (acts:list action) : action :=
match acts, svo with
nil , GlobalAction l => Action (Message l Emit nil) nil
| Action (Message _m _ct lp) _asngs :: _ , GlobalAction l => Action (Message l Emit lp) nil
end.
The function global_action_output returns the resulting global action w.r.t.
the activated synchronization vector and the actions ocurring at the involved LTS objects.
Function at_least_one_emit (acts:list action) : option parameters :=
match acts with
nil => None
| Action (Message m Read lp) _asngs :: r => at_least_one_emit r
| Action (Message m Emit lp) _asngs :: r => Some lp
end.
Function read_match (lp:parameters) (lp':parameters) : bool :=
match lp, lp' with
nil , nil => true
| p :: r, p' :: r' => match p, p' with
Val n, Val m => if beq_nat n m then read_match r r' else false
| Val n, Var x => read_match r r'
| _ , _ => false
end
| _ , _ => false
end.
Function emit_match (lp:parameters) (lp':parameters) : bool :=
match lp, lp' with
nil , nil => true
| p :: r, p' :: r' => match p, p' with
Val n, Val m => if beq_nat n m then read_match r r' else false
| _ , _ => false
end
| _ , _ => false
end.
Function match_parameters (acts:list action) (lp:parameters) : bool :=
match acts with
nil => true
| Action (Message m Read lp') _asngs :: r => read_match lp lp'
| Action (Message m Emit lp') _asngs :: r => emit_match lp lp'
end.
Function is_compatible (acts:list action) : bool :=
match at_least_one_emit acts with
None => false
| Some lp => match_parameters acts lp
end.
Function exclude_incompatible_parameter_messages (lacts:list (list action)) : list (list action) :=
match lacts with
nil => nil
| acts :: r => if is_compatible acts then
acts :: exclude_incompatible_parameter_messages r
else
exclude_incompatible_parameter_messages r
end.
The function exclude_incompatible_parameter_messages is responsible for filtering
the incompatible actions combinations w.r.t. the specified parameters.
Function var_valuations (lp: parameters) (q:lts_state) : parameters :=
match lp with
nil => nil
| Val n :: r => Val n :: var_valuations r q
| Var x :: r => match q with
LTS_State i mem => let n := valuation x mem in
Val n :: var_valuations r q
end
end.
Function treat_synch_emissions (acts: list action) (qs:lts_states) : list action :=
match acts, qs with
nil , nil => nil
| Action (Message m ct lp) asngs :: r, q :: rq =>
match ct with
Read => Action (Message m ct lp) asngs :: treat_synch_emissions r rq
| Emit => Action (Message m ct (var_valuations lp q)) asngs :: treat_synch_emissions r rq
end
| _, _ => nil
end.
Function treat_emissions (lacts: list (list action)) (qs:lts_states) : list (list action) :=
match lacts with
nil => nil
| acts :: r => treat_synch_emissions acts qs :: treat_emissions r qs
end.
The function treat_emissions simply makes sure we emit the valuations and not variables references,
i.e., we always emit actual values.
Fixpoint net_target_states (net_obj : Net) (q: net_state) (sv:SynchronizationVector) : list (action * net_state) :=
match net_obj, q, sv with
mk_Net (list_lts, list_svs) , Net_State list_lts_states,
SyncVector (sv_elements, sv_output) =>
let acts := allowed_actions_from_sv_element list_lts list_lts_states sv_elements in
let acts' := combineN acts in
let acts' := treat_emissions acts' list_lts_states in
let acts' := exclude_incompatible_parameter_messages acts' in
(fix fix_net_target_states (list_acts: list (list action)) :=
match list_acts with
nil => nil
| acts :: r =>
let no_msg_lts_states := get_target_lts_states list_lts_states list_lts acts in
let params_to_emit := message_parameter_to_emit no_msg_lts_states in
let list_lts' := transmit_message params_to_emit no_msg_lts_states in
let global_action := global_action_output sv_output acts in
(global_action, Net_State (list_lts')) :: fix_net_target_states r
end) acts'
| _, _, _ => nil
end.
The function net_target_states computes the attained net_states along
with the global action resulting from the activated SynchronizationVector.
Inductive indexed_membership (list_lts_st: list lts_state)
(list_lts: list LTS) : Prop :=
| IM0 : list_lts_st = nil ->
list_lts = nil ->
indexed_membership list_lts_st list_lts
| IMn : forall st r lts_obj r',
list_lts_st = st :: r ->
list_lts = lts_obj :: r' ->
In st (@States lts_obj) ->
indexed_membership r r' ->
indexed_membership list_lts_st list_lts.
The indexed_membership specifies a membership relation between the elements of the
list given as parameter. It shall be useful for performing proofs.
Function get_list_snd (X:Type) (Y:Type) (l: list (X * Y)) : list Y :=
match l with
nil => nil
| (a,b) :: r => b :: get_list_snd r
end.
The above function shall be useful at a later stage. It will be used
whenever we solely want to refer to the net_states returned by
the net_target_states function.
Definition init_net_state (net_obj: Net) : net_state :=
match net_obj with
mk_SingletonNet lts_obj => NetSingleton_State (@Init lts_obj)
| mk_Net (list_lts, _svs) =>
let lq := (fix fix_init_lts_states list_lts :=
match list_lts with
nil => nil
| lts_obj :: r => (@Init lts_obj) :: fix_init_lts_states r
end
) list_lts in
Net_State lq
end.
As the name indicates, the above function, init_net_state, computes
the initial net_state of a Net system. It is rather simple:
it is composed by a single or several initial lts_states of the
LTS objects composing the Net.
Function seen (q:net_state) (mem:list net_state) : Prop :=
match mem with
nil => False
| q':: r => match q', q with
NetSingleton_State s, NetSingleton_State s' =>
if s === s' then True else seen q r
| Net_State lq, Net_State lq' =>
let x := (fix fix_seen lq lq' :=
match lq, lq' with
nil, nil => true
| qq :: rr, qq' :: rr' => if qq === qq' then fix_seen rr rr' else false
| _, _ => false
end) lq lq' in
if x then True else seen q r
| _, _ => seen q r
end
end.
Inductive attainable (A:Net) : list net_state -> net_state -> net_state -> Prop :=
| Attain0 : forall q mem, q=q -> attainable A mem q q
| AttainN : forall qi qf,
forall mem, ~ seen qi mem ->
forall list_lts svs, A = mk_Net (list_lts, svs) ->
forall qn sv,
In sv svs ->
forall ga_lq, ga_lq = net_target_states A qi sv ->
In qn (get_list_snd ga_lq) ->
attainable A (qi::mem) qn qf ->
attainable A mem qi qf.
The predicate attainable specifies that two net_states are attainable.
It uses a simple memory of already seen net_states in order to avoid loops.
Finally, we are in a position to define the Net_Trace predicate.
It is defined co-inductively, as we deal with potentially infinite
execution traces. Its three constructors account for all the cases it
has to deal: composed by a single LTS, reached a deadlock, going to
a state among those that are attainable by the activated synchronization
vector.
CoInductive Net_Trace (A: Net) : net_state -> LList action -> Prop :=
| lts_trace: forall net_q lts_q,
net_q = NetSingleton_State lts_q ->
forall A', A=mk_SingletonNet A' ->
In lts_q (@States A') ->
forall l, LTS_Trace A' lts_q l ->
Net_Trace A net_q l
| net_empty_trace:
forall (q:net_state),
forall list_lts list_sv,
A = mk_Net (list_lts, list_sv) ->
forall list_lts_states, q = Net_State list_lts_states ->
indexed_membership list_lts_states list_lts ->
attainable A nil (init_net_state A) q ->
(forall sv, In sv list_sv -> net_target_states A q sv = nil) ->
Net_Trace A q LNil
| net_lcons_trace:
forall (q:net_state) l,
forall (sync_vec:SynchronizationVector) list_lts list_sv,
A = mk_Net (list_lts, list_sv) ->
forall list_lts_states, q = Net_State list_lts_states ->
indexed_membership list_lts_states list_lts ->
attainable A nil (init_net_state A) q ->
In sync_vec list_sv ->
forall ga_lq', ga_lq' = net_target_states A q sync_vec ->
forall ga q', In (ga, q') ga_lq' -> Net_Trace A q' l ->
Net_Trace A q (LCons ga l).