Simulator

What follows is the ACL2 simulator of CAETI systems from Model 1, modified by replacing "TCP socket" terminology by "CAETI address" terminology. It still needs to be updated to include the other differences between Model 1 and Model 2. 

in-package("ACL2");
/* We need the concrete version of a-caeti-address for simulation. */

type a-caeti-address = integer;

type a-CMA-type = enum[ tell, ask, do, subscribe, sorry ];

type a-CMA-msg =
 record (kind : a-CMA-type,
         sender : a-caeti-address,
         receiver : a-caeti-address,
         content  : string,
         language : string := "text",
         ontology : string,
         reply-with  : string,
         in-reply-to : string);

type a-CMA-history = a-CMA-msg * ;        /* A list of a-CMA-msg */

type an-in-out = record ( inl : a-CMA-history, outl : a-CMA-history );

type a-caeti-system = [ a-caeti-address . an-in-out ] *;

theorem caeti-system-true-list
 { a-caeti-system(x) -> true-listp(x) };

function is-unique-caeti-address (s : a-caeti-address, l : a-caeti-system) : boolean 
 { ~(l \ s) };

function all-caeti-addresss-unique (l)
{ if ~consp(l)
    then t 
  elif a-caeti-system(l) & is-unique-caeti-address(l.car.car, l.cdr)
    then all-caeti-addresss-unique(l.cdr)
  else nil };

verify guards all-caeti-addresss-unique;

function is-caeti-system (l : a-caeti-system) : boolean 
 { all-caeti-addresss-unique(l) };
/* Update incoming and outgoing message histories. Given a msg and a CAETI-system we update the history for the addresses of msg by adding msg to its sender's outgoing-msg field. If there is no outgoing history corresponding to the sender of msg, we make an empty one and add msg to its outgoing-msg field. */

function update-outgoing-msg (msg : a-CMA-msg ,
			      s : a-caeti-system): a-caeti-system
/* The nil in make-an-in-out is the empty input history. */
{ if endp(s) then [ sender(msg) :> make-an-in-out(nil , [msg]) ]
  elif msg.sender = car(s.car)
    then cons( s.car.car :> update-an-in-out(s.car.cdr, :outl cons(msg, outl(s.car.cdr))),
	          s.cdr)
  else s.car :> update-outgoing-msg(msg, s.cdr) };

function update-incoming-msg (msg : a-CMA-msg ,
			      s : a-caeti-system): a-caeti-system
{ if endp(s) then [ receiver(msg) :> make-an-in-out([msg] , nil) ]
  elif receiver(msg) = s.car.car
    then cons( s.car.car :> update-an-in-out(s.car.cdr, :inl cons(msg, inl(s.car.cdr))),
	          s.cdr)
  else cons(s.car, update-incoming-msg(msg, s.cdr)) };
/* Given a msg from sender to receiver we update the outgoing-msg field of the sender and the incoming-msg field of the receiver. This is the fundamental "transaction" on a CAETI-system, s. */

function update-caeti-system (msg : a-CMA-msg, s : a-caeti-system): a-caeti-system
{  update-incoming-msg (msg, update-outgoing-msg (msg, s)) };

function caeti-sim ( l : a-CMA-history, s : a-caeti-system): a-caeti-system
{ if endp(l) then s
  else caeti-sim(l.cdr, update-caeti-system(l.car, s)) };
/* Here is a sample call. */

caeti-sim(
'[ [MAKE-A-CMA-MSG, tell,  1, 2, "msg a from 1 to 2", "text", "text", "", ""],
   [MAKE-A-CMA-MSG, ask,   2, 1, "query from 2 to 1", "text", "text", "", ""],
   [MAKE-A-CMA-MSG, tell,  1, 2, "response from 1 to 2", "text", "text", "", ""],
   [MAKE-A-CMA-MSG, ask,   3, 1, "query from 3 to 1", "text", "text", "", ""],
   [MAKE-A-CMA-MSG, sorry, 3, 1, "failure report 3 to 1", "text", "text", "", ""]],
 nil);
/* Here is the result with some comments: 

((1 ; List of messages received, in reverse chronological order:
    ((TYPE1 . "Reply from 3 to 1 about their first message.")
     (TYPE1 . "Reply from 2 to 1 about first message."))
    ; List of messages sent, in reverse chronological order:
    ((TYPE1 . "First message from 1 to 3.")
     (TYPE1 . "First message from 1 to 2.")))
 (2 ; List of messages received, in reverse chronological order:
    ((TYPE1 . "First message from 1 to 2."))
    ; List of messages sent, in reverse chronological order:
    ((TYPE1 . "Spontaneous message from 2 to 3.")
     (TYPE1 . "Reply from 2 to 1 about first message.")))
 (3 ; List of messages received, in reverse chronological order:
    ((TYPE1 . "Spontaneous message from 2 to 3.")
     (TYPE1 . "First message from 1 to 3."))
    ; List of messages sent, in reverse chronological order:
    ((TYPE1 . "Reply from 3 to 1 about their first message."))))

*/
This page is URL http://www.computationallogic.com/software/caeti/architecture/model/simulator.html