------------------------------ MODULE serie3_2 ------------------------------
EXTENDS Naturals
CONSTANT Data,N
VARIABLES dch,file,s

TypeInvariant == 
  file  \subseteq Nat \X Nat /\ dch \subseteq Nat \X Nat  /\ s \in Nat   
--------------------------------------------------------------

FILE ==  [i \in Data  |->  i]



Init ==  file ={} /\ dch = {} /\ s=1 


sndd ==  /\  s <  N+1 
         /\  dch'  = dch \cup { <<s,FILE[s]>>} 
         /\  s'=s+1
         /\  file'=file

rcvd ==   
 /\  dch # {}
 /\ LET  v == CHOOSE <<i,val>> \in  Data \X Data  :    <<i,val>> \in dch
    IN  
            /\  file' =  file \cup {<<v[1],v[2]>>} 
            /\  dch' = dch \ {<<v[1],v[2]>>} 
            /\  s' = s


loose == 
 /\ \E v \in Data : \E i \in Data:   <<i,v>> \in dch
 /\ LET  v == CHOOSE <<i,val>> \in  Data \X Data  :    <<i,val>> \in dch
    IN 
            /\  <<v[1],v[2]>> \in dch
            /\  file' =  file 
            /\  dch' = dch \ {<<v[1],v[2]>>}  
            /\  s' = s
            /\  file'=file



Next == sndd \/ rcvd  (*  \/ loose *)

Spec == Init /\ [][Next]_<<dch,file,s>>


invariant == (dch \cup file = { <<i,v>> \in Data \X Data : i \leq s-1 /\ v=FILE[i]}) 

--------------------------------------------------------------
THEOREM Spec => []TypeInvariant
=============================================================================
\* Modification History
\* Last modified Mon Jan 25 15:21:01 CET 2016 by arthur
\* Created Mon Jan 25 14:55:26 CET 2016 by arthur