From VLSM.Lib Require Import Itauto.
From stdpp Require Import prelude.
From VLSM.Lib Require Import Preamble StreamExtras StreamFilters StdppExtras.
From VLSM.Core Require Import VLSM VLSMProjections.VLSMPartialProjection.

Core: VLSM Stuttering Embeddings

Stuttering embeddings are VLSM projections guaranteeing the existence of translations for all states and traces, in which a transition in the source VLSM translates to a (possibly empty) sequence of transitions in the target VLSM.

A stuttering embedding is established from VLSM X to VLSM Y (sharing the same messages) if there exists maps state_project taking X-states to Y-states, and transition_item_project, taking a transition from X to a list of transitions in Y, such that:

transition_item_project_consistency: the state-translation of the destination of a transition is the final state of the translation of the transition.
stuttering_embedding_preserves_valid_traces: traces obtained by concatenating the translations of transition of a valid trace are valid.

An example of proper stuttering embedding is given by a VLSM summarizing the transitions of another VLSM.

Stuttering embedding definitions and properties

Any VLSM_stuttering_embedding_type determines a VLSM_partial_projection_type, allowing us to lift to VLSM stuttering embeddings the generic results proved about VLSM partial projections.

Similarly to the VLSM_partial_projection case we distinguish two types of stuttering embeddings: VLSM_weak_stuttering_embedding and VLSM_stuttering_embedding, distinguished by the fact that the weak embeddings are not required to preserve initial states.

Here we restate the pre_ definitions above to depend on VLSM_weak_stuttering_embedding and have their state and transition item projection functions implicit.

While for the above section, the VLSM_weak_stuttering_embedding was necessary to be mentioned explicitly, in the following we make it part of the context.

Any VLSM_weak_stuttering_embedding determines a VLSM_weak_partial_projection, allowing us to lift to weak stuttering embeddings the generic results proved about weak partial projections.

Here we restate the pre_ definitions above to depend on VLSM_stuttering_embedding and have their state and transition item projection functions implicit.

While for the above section, the VLSM_stuttering_embedding was necessary to be mentioned explicitly, in the following we make it part of the context.

Any VLSM_stuttering_embedding determines a VLSM_partial_projection, allowing us to lift to stuttering embeddings the generic results proved about partial projections.

Stuttering embedding friendliness

A stuttering embedding is friendly if all the valid traces of the destination VLSM are prefixes of translations of the valid traces of the source VLSM.

Section sec_stuttering_embedding_friendliness.

We axiomatize stuttering embedding friendliness as the converse of VLSM_stuttering_embedding_finite_valid_trace. However, since a transition in the source corresponds to possibly multiple transitions in the destination, we'll ask that any valid trace in the destination is the prefix of a translation of a valid trace from the source.

Definition stuttering_embedding_friendly_prop : Prop :=
  forall
    (sY : state Y)
    (trY : list (transition_item Y))
    (HtrY : finite_valid_trace Y sY trY),
  exists (sX : state X) (trX : list (transition_item X)),
    finite_valid_trace X sX trX
    /\ state_project sX = sY
    /\ trY `prefix_of` VLSM_stuttering_embedding_finite_trace_project Hsimul trX.

Lemma stuttering_embedding_friendly_finite_valid_trace_from_to
  (Hfr : stuttering_embedding_friendly_prop)
  (sY1 sY2 : state Y) (trY : list (transition_item Y))
  (HtrY : finite_valid_trace_from_to Y sY1 sY2 trY)
  : exists (sX1 sX2 : state X) (trX : list (transition_item X))
      (preY sufY : list (transition_item Y)),
      finite_valid_trace_from_to X sX1 sX2 trX /\
      VLSM_stuttering_embedding_finite_trace_project Hsimul trX = preY ++ trY ++ sufY.
Proof.
  apply finite_valid_trace_from_to_complete_left in HtrY
    as (is & tr_s1 & Htr & _).
  apply valid_trace_forget_last, Hfr in Htr as [isX [trX [[Htr _] [His [suf Htr_pr]]]]].
  exists isX, (finite_trace_last isX trX), trX, tr_s1, suf.
  split.
  - by apply valid_trace_add_default_last.
  - by rewrite app_assoc.
Qed.

A consequence of the stuttering_embedding_friendly_property is that the valid traces of the target VLSM are precisely prefixes of translations of all the valid traces of the source VLSM.

Lemma stuttering_embedding_friendly_trace_char
  (Hfriendly : stuttering_embedding_friendly_prop)
  : forall sY trY, finite_valid_trace Y sY trY <->
    exists (sX : state X) (trX : list (transition_item X)),
    finite_valid_trace X sX trX
    /\ state_project sX = sY
    /\ trY `prefix_of` VLSM_stuttering_embedding_finite_trace_project Hsimul trX.
Proof.
  split; [by apply Hfriendly |].
  intros (sX & trX & HtrX & <- & sufY & HtrY).
  apply VLSM_stuttering_embedding_finite_valid_trace in HtrX as [HtrX].
  split; [| done].
  eapply finite_valid_trace_from_app_iff.
  by rewrite <- HtrY.
Qed.

End sec_stuttering_embedding_friendliness.

End sec_stuttering_embedding_properties.

To establish a stuttering embedding from VLSM X to VLSM Y, the following set of conditions is sufficient:

X's initial_states project to Y's initial states
Every input-valid transition translates to a valid trace from the translation of the source of the transition to the translation of the destination of the transition