The Coq mailing list

[Nuno Gaspar <nmpgaspar AT gmail.com>]

Hello, 

I'm trying to model the behavior of a very simple system. Consider the following

Inductive system_exec : message -> state -> state -> Prop :=
  | Request: forall (s s' : state) (m : message),
            q m s ->
            s' = send_request m s ->
         system_exec  m s s'
             
  | Reply: forall (s s' : state) (m : message),
                  p m s ->
                  s' = send_reply m s ->
       system_exec  m s s'

(*p and q are just predicates included here for the sake of clarity..*)

where state is a structure along the lines of an automaton.

The idea is that I want to model a (possibly infinite) execution, meaning an infinite number of messages sent, making it go from state s to state s'...

If following the standard approach used for operational semantics, I would use a (possibly refl.) transitive closure of system_exec, but I cannot use this in this case as I'm not going from elements of the same type. I mean its not like I can do (message * state) -> (message * state) as the message on the 'target' state is senseless for my modeling...

Also, usually one uses this approach to model the fact of program 'reduction', until we cannot progress anymore (e.g. SKIP - well if you define your relation reflexive you can still progress, but lets ignore that...), which is not exactly what I want here.

So, how would you go about modeling a system that would just allow a 
possibly infinite exchange of messages in a operational semantics 
fashion?


One possible idea would be defining my relation from (stream message * state) to (stream message * state). Then, my Request constructor would take the head of the stream to know the message to send, and would go to a state s' with the effect of that emission. As for the Reply constructor, it would just check if there is some message to reply to, affect the state and leave the stream of messages unaffected I guess.. 

Well, I still need some thinking on this, but anyway, do you think the above would be a good approach? How would you do it? :D

Thank you, and an Happy New Year to all of you who just got back to the office today!

Cheers.

-- 
Bart: Look at me, I'm a grad student, I'm 30 years old and I made $600 dollars last year.
Marge: Bart! Don't make fun of grad students, they just made a terrible life choice.