Apims

From thelas.dk

Jump to: navigation, search
A screenshot of the user-interfase presented by a sample apims program
A screenshot of the user-interfase presented by a sample apims program

Apims is an early version of HAPI.

Apims is an interpretor and typechecker for the Asynchronous PI-calculus with Multiparty sessions and Symmetric synchronization. The key feature of this interpretor is the symmetric sum types that allow type checking of the GUI's implemented using the symmetric synchronization. From version 2.0.0 apims has support for type assertions, that enables restrictions on the communicated values and choices to be specified by logical predicates (as propositional formulas).

Apims has been developed as a proof of concept implementation of some of the theoretical work I have done in my PhD project. Since this is a proof of concept implementation, the users should be prepared to find bugs, but currently there are no known bugs.

apims is a c++ library, but contains sample programs to typecheck and evaluate code. The installation instructions includes an example of how to evaluate code.

Contents

Requirements

  • DynParser is used to parse the given programs.
  • libpi is used by the generated c++ code, and is thus required for generatin executables.
  • GMP - the gnu multi-precission arithmetics library.
  • SDL and in particular the network library libsdl-net is used to start a webserver that allows user-interaction with the running processes.

Versions / Download

Get the newest verions from the apims repository.

Installation Instructions

Apims can be installed using the package apims in the deb repository.

If you wish to manually compile the library and programs, the procedure is as follows

tar -xvzf apims-1.5.0.tgz
cd apims-1.5.0
make config
make build
sudo make install
cd programs
make config
make build
sudo make install
cd ..
cd apims_examples
cd hello_world
make build
./hellow_world

Now the installation procedure will be explained in more detail.

Before installing the apims library, make sure you have installed the requirements.

When the necessary dependencies have been installed, apims is downloaded using the above link.
The rest of the installation is done using a shell or terminal.

To unpack the downloaded file, go to the directory containing the downloaded file and execute tar -xvzf apims-1.5.0.tgz.
Then enter the created folder by executing cd apims-1.5.0.
Now it is time to create a Makefile from the Makefile.in by typing make config.
The apims library can now be compiled by typing make build.
Finally install the library by executing make install as root.

If no errors were encountered the project is now installed, and you can start using the library.

To install the apims interpretor, enter the programs folder by typing cd programs.
Then build the interpretor in the same way as the library, by executing make config, make build and finally make install as root.

Now the interpretor is installed, and it can be used to evaluate programs.
An array of sample programs are in the apims_code folder. Enter this folder by typing cd apims_code.
Now evaluate the example.mps program by typing apims -f example.mps. This will evaluate the sampel program, writing each step in the evaluation to the console.

VM Disk image

There is a VM disk image available here. It is a stripped version of debian, with apims and it dependencies checked out from github, compiled and installed ready to use. The disk image should be usable from all VMs including VMWare and Virtualbox. Be aware that VMs oly can use the hardware assigned to it, so multicore utilization will require some specific configuration of the VM.

Login

User: apims
Password: apims

Usage

Configure a VM with the downloaded disk image as the main disk, boot and login.

The Apims source code and examples are in the /home/apims/projects/apims folder.

Documentation

The source code is fairly well commented, and the comments have been extracted to documentation using Doxygen. The extracted documentation is available here.

For information on installing apims, use the installation instructions above, and for information on writing apims programs, see the tutorial below.

Tutorial

Apims is build on the pi-calculus with multiparty session types. This is fundamentally different from most programming languages, and therefore apims may seem like a strange language at first. This approach however means that apims gains from the extensive research invested in the pi-calculus, offering the programmer and user some unique guarantees.

The basic concepts in apims are processes, channels, messages and sessions. Basically a process is a program. It can communicate with other processes by sending messages over channels. Now we just need to understand what sessions are. A session is a collection of channels that follow a specified network-protocol. In stead of using many pages to explain these concepts in detail as it is done on wikipedia, this section will in stead give a number of examples to develop the intuitive understanding of the language.

Starting a session

(nu a: Gend)
( link(2,a,s,1);
  end
| link(2,a,s,2);
  end
)

The above example is actually two processes. The first process link(2,a,s,1);end uses channel a to create the session s with two participants where the process is participant nr. 1, and then the process ends.
The second process link(2,a,s,2);end uses channel a to create the session s with two participants where the process is participant nr. 2, and then the process ends.
The (nu a: Gend) specifies that the channel a can be used to create sessions on, and Gend is the protocol of the created sessions. Gend is the name of the completed protocol, and this means that no messages can (or must) be sent on the sessions created on a.

Sending a message

(nu a: 1=>2<Int>;Gend)
( link(2,a,s,1);
  s[2]<<5;
  end
| link(2,a,s,2);
  s[1]>>x;
  end
)

The above example is similar to the first example, and consists of two processes. The first process link(2,a,s,1);s[2]<<5;end creates the session s on channel a, and continues as participant 1 out of 2. Then the process sends the integer 5 to participant number 2 in session s, and then the process ends.
The second process link(2,a,s,2);s[1]>>x;end creates the session s on channel a, and continues as participant 2 out of 2. Then the process receives a message from participant 1 in session s, stores the value in the variable 'x', and then the process ends.
In this example, the channel 'a' can no longer use the protocol Gend since a message will be sent over the created session. Therefore the channel is declared as (nu a: 1=>2:1<Int>;Gend) which means that first participant 1 sends a message with an integer to participant 2 on channel 1, and then the protocol is completed.

A simple server

(nu a : 1=>2:1
        { ^sum: 1=>2:1<Int>;
                1=>2:1<Int>;
                2=>1:2<Int>;
                Gend,
          ^mult:1=>2:1<Int>;
                1=>2:1<Int>;
                2=>1:2<Int>;
                Gend,
          ^neg: 1=>2:1<Int>;
                2=>1:2<Int>;
                Gend
        })
( def X(var: Int) =
    link(2,a,s,2);
    ( X(var)
    | s[1] >>
      { ^sum: s[1] >> x;
              s[1] >> y;
              s[2] << x+y;
              end,
        ^mult:s[1] >> x;
              s[1] >> y;
              s[2] << x*y;
              end,
        ^neg: s[1] >> x;
              s[2] << 0-x;
              end
      }
    )
  in X(0)
| link(2,a,s,1);
  s[1] << ^mult;
  s[1] << 5;
  s[1] << 3;
  s[2] >> x;
  link(2,a,s,1);
  s[1] << ^sum;
  s[1] << x;
  s[1] << x;
  s[2] >> x;
  link(2,a,s,1);
  s[1] << ^neg;
  s[1] << x;
  s[2] >> x;
  end
)

The above code consiste of two processes, but lets start with the protocol they use to communicate.
First participant 1 (the client) sends a message to participant number two (the server) on channel 1.
This message selects between three ways the communication can continue, identified by three labels.
If the client sends the label ^sum or ^mult then the client must send two integers to the server on channel 1 before the server sends an integer to the client on channel 2.
If the client sends the label ^neg then the client must send an integers to the server on channel 1 before the server sends an integer to the client on channel 2.

The first process is the server. It creates the session s over channel a, and continues as participant 2.
As soon as the session is created, it forks into two processes, where the first waits for a new connection, and the second completes the new session.
The session is completed by branching on channel 1. This means that it receives a label, and how it continues is based on the received label.
If the label ^sum is received, it receives two integers on channel 1, and sends their sum on channel 2.
If the label ^mult is received, it receives two integers on channel 1, and sends their product on channel 2.
If the label ^neg is received, it receives one integer on channel 1, and sends the negated value on channel 2.

The second process acts as the client. By connecting to the server three times, it calculates the value of -((5*3)+(5*3)).

Persistent Server

(nu a : rec $server.
        1=>2:1
        { ^add: 1=>2:1<Int>;
                $server,
          ^mult:1=>2:1<Int>;
                $server,
          ^neg: $server,
          ^done:2=>1:2<Int>;
                Gend
        })
( def Fork(id: Int) =
    link(2,a,s,2);
    ( Fork(id+1)
    | def Server(s: rec %server.
                    1 >>
                    { ^add: 1>><Int>;
                            %server,
                      ^mult:1>><Int>;
                            %server,
                      ^neg: %server,
                      ^done:2<<<Int>;
                            Lend
                    }@(2of2),
                 v: Int) =
        s[1] >>
        { ^add: s[1] >> x;
                Server(s,v+x),
          ^mult:s[1] >> x;
                Server(s,v*x),
          ^neg: Server(s,0-v),
          ^done:s[2]<<v;
                end
      }
      in Server(s,0)
    )
  in Fork(1)
| link(2,a,s,1);
  s[1] << ^add;
  s[1] << 5;
  s[1] << ^mult;
  s[1] << 3;
  s[1] << ^mult;
  s[1] << 2;
  s[1] << ^neg;
  s[1] << ^done;
  s[2] >> x;
  end
)

The above example is a calculation server, and a client that performs the same calculation as the previous example.
The difference from the previous example is that it is no longer necessary to connect to the server three times to perform the calculation. In stead of ending the connection when the first calculation has been performed, the connection continues to with calculations, until the label ^done chosen, after which the server sends the accumulated result to the client and the session ends.
Notice that this change requires the session to be recursive.

Guessing game

(nu a: 1=>3:1<Bool>;
       2=>3:2<Bool>;
       3=>1:3<String>;
       3=>2:4<String>;
       Gend)
( // The judge
  link(3,a,s,3);
  s[1] >> v1;
  s[2] >> v2;
  if (v1 and not v2) or (v2 and not v1) // Has player 2 won
  then
  ( s[3] << "Sorry, player 2 has won";
    s[4] << "Congratulations";
    end
  )
  else
  ( s[3] << "Congratulations";
    s[4] << "Sorry, player 1 has won";
    end
  )
| // Player 1
  link(3,a,s,1);
  s[1] << true;
  s[3] >> x;
  end
| // Player 2
  link(3,a,s,2);
  s[2] << false;
  s[4] >> x;
  end
)

In this example two players each sends a boolean value to a judge. The judge decides who has won the game depending on both values, and sends the results to the players. This example shows how simple it is to write sessions with more than two participants.

Symmetric Sumtypes

Social interactions are interactions among people as well as human organisations, as opposed to interactions among computer processes.

Social interactions include workflow models and various cooperation models, and serve as a basis of many application-level protocols in computing such as healthcare and financial protocols. Just like their computer counterparts, social interactions are often highly structured, coming from the underlying social, economic and legal concerns.

There is richness in social interaction structures, stemming from diverse collaborative patterns people and human organisations can exhibit. One of such pattern is for multiple participants in an interaction to collectively decide on one of the possible choices, as found in many implicit and explicit group-based agreements.

The essence of this interaction pattern is a phase inside a conversation where a group of participants collectively wish to decide on one of the possible choices, and when they decide, they collectively commit to that option. One might call such an interaction pattern, symmetric synchronisation because all the participants are equal in the decision-making.

Apims supports symmetric synchronisation in sessions, and the protocols are described by symmetric sum types.

Synchronization

Apims represents a specific social interaction, best described as a plenum decision, where all the participants must agree on one ofApims supports a simple kind of social interaction, where a choice is made my agreement between the participants in a session.
This is expressed using a sync process, where a number of process must continue with a common label.

A synch process has the form

synch(n,t) {li: Pi}

and is interpreted as the process participating in a plenum decision between n processes in the session t reaching a common decision li for some i. Afterwards the process proceeds as described in Pi.

Sum Types

In order to describe the plenum decision behaviour, and allow synchronisation processes, Apims includes Symmetric Sum Types.

Symmetric sum types are of the form

{ li: Gi }

where there is at least one label li of the form ^name (starting with a ^). the labels starting with ^ are called the mandatory labels (M), and the labels starting with # are called the optional labels (L).
The mandatory and must be accepted by all the participants.

The well-typed processes behave well in the way that they can always agree on some branch (thus they never disagree), and each process will not skip a synchronisation, or use a synchronisation that is not described in the protocol.

Example

The synchronisation and sum types are explained in the paper on Symmetric Sum Types, but we give a small example here, to explain how they work in Apims.

  // The Choreography
  // Patient: 1
  // Doctor: 2
  // Nurse: 3
(nu a : { #case1: 1=>2:1<String>;
                  2=>1:2<String>;
                  2=>1:3<String>;
                  Gend,
          ^case2: 1=>3:1<String>;
                  2=>1:2<String>;
                  2=>1:3<String>;
                  Gend,
          #case3: 1=>2:1<String>;
                  3=>1:2<String>;
                  2=>1:3<String>;
                  Gend,
          #case4: 1=>3:1<String>;
                  3=>1:2<String>;
                  2=>1:3<String>;
                  Gend })
( // The Patient
  link(3,a,t,1);
  sync(3,t)
  { #case1: t[1]<<"headache";
            t[2]>>time;
            t[3]>>result;
            end,
    ^case2: t[1]<<"headache";
            t[2]>>time;
            t[3]>>result;
            end,
    #case3: t[1]<<"headache";
            t[2]>>time;
            t[3]>>result;
            end,
    #case4: t[1]<<"headache";
            t[2]>>time;
            t[3]>>result;
            end
  }
| // The Doctor
  link(3,a,s,2);
  sync(3,s)
  { #case1: s[1]>>data;
            s[2]<<"now";
            s[3]<<"diagnose: concussion";
            end,
    ^case2: s[2]<<"now";
            s[3]<<"diagnose: concussion";
            end,
    #case4: s[3]<<"diagnose: consussion";
            end
  }
| // The Nurse
  link(3,a,r,3);
  sync(3,r)
  { #case1: end,
    ^case2: r[1]>>data;
            end,
    #case3: r[2]<<"now";
            end
  }
)

This example first describes a choreography, explaining how three participants (a patient, a doctor and a nurse) cooperates, where they first agree on one of four cases, and then continues with the agreed case. Then the implementation of each participant is given, where the doctor does not accept the third case, and the nurse does not accept the fourth case. This means that the cases that can be selected are the mandatory case (case two) and case 1.

User Interaction

Under construction!

In order for users to interact with the programs, the language has two terms called guisync and guivalue. Each participant of each session has its own user interface, and the gui terms are used to define these interfaces in a declarative way.

The term guisync is an gui version of the synch term, which displays the choices to the user, and accepts inputs for each choice. In this way the user can influence the chosen branch and thus how the process procedes.

The use of guisync is the same as for synch except the process id is given as an additional argument, and the choices can use arguments which are supplied by the user before the choice can proceed. This results in the syntax below.

guisync(maxpid,session,pid){ li(args): Pi }

The guisync terms are typed in the same way as the synch terms.

The term guivalue is used to add information to a user interface, and the arguments are the number of participants of the session, the session name, the participant number, the name of the value, and the value itself. This results in the syntax below.

guivalue(maxpid,session,pid,"name",exp);P

Simple User Interface Examples

The first gui example we will show is a simple faculty calculation. This example has two processes. The first process is the server, which accepts a connection, receives an input, calculates the faculty of the given input and sends the result back. The second process is the user interface. Notice that the user interface also has a session type, which describes the allowed choices. The user interfaces presents the user with a single choice (^Fact) which requires an integer input. Then the input is wntered and the user presses "Accept", the process connects to the server process, sends the given input, receives the result, displays it using the guivalue term, and waits for the user to quit.

Image:Apims-gui-fact1a.png
A screenshot of the user interface implemented in this example
Image:Apims-gui-fact1b.png
A screenshot of the user interface implemented in this example
(nu a : 1=>2:1<Int>;2=>1:2<Int>;Gend)      // Fact Server Protocol
( link(2,a,s,2);                           // Receive Connection
  s[1] >> x;                               // Receive argument
  def Fact(n: Int, acc: Int,               // Define Fact Function
           dest: 2<<<Int>;Lend@(2of2)) =
      if n=1                               // If simple case
      then dest[2] << acc;end              // Send accumulated value
      else Fact(n-1, acc*n, dest)          // Else make recursive call
  in Fact(x,1,s)                           // Call Fact Function
| (nu gui: {^Fact: {^Quit: Gend} })        // User Interface Behavior
  ( link(1,gui,user,1);                    // Create User Interface
    guisync(1,user,1)                      // Wait for User Input
    {^Fact(n: Int):                        // Request n
      link(2,a,s,1);                       // Connect to Fact Server
      s[1] << n;                           // Send n
      s[2] >> result;                      // Receive n!
      guivalue(1,user,1,"Fact:",result);   // Add result to User Interface
      guisync(1,user,1)                    // Wait for user to quit
      {^Quit(comment: String): end }
    }
) )

In the next example, the calculation of the factorial is carried out in a different way, where a new process is spawned and invoked for each recursive call. Notice however that the user interface process remains unchanged, because it just communicates the the argument and result with the server and is thus independant on the way the result is calculated.

(nu a : 1=>2:1<Int>;2=>1:2<Int>;Gend)    // Fact Server protocol
( def Fact() =                           // Define Fact Server
      link(2,a,s,2);                     // Receive Connection
      ( Fact()                           // Start new server
      | s[1] >> x;                       // Receive argument
        if x=1                           // If simple case
        then s[2] << 1;end               // Return directly
        else link(2,a,t,1);              // Connect to (another) Fact Server
             t[1]<<x-1;                  // Send x-1
             t[2]>>y;                    // Receive (x-1)!
             s[2]<<y*x;                  // Send result (x-1)!*x
             end
      )
  in Fact()                              // Start Fact Server
| (nu gui: {^Fact: {^Quit: Gend} })      // User Interface Behavior
  ( link(1,gui,user,1);                  // Create User Interface
    guisync(1,user,1)                    // Wait for User Input
    {^Fact(n: Int):                      // Request n
      link(2,a,s,1);                     // Connect to Fact Server
      s[1] << n;                         // Send n
      s[2] >> result;                    // Receive n!
      guivalue(1,user,1,"Fact:",result); // Add result to User Interface
      guisync(1,user,1)                  // Wait for user to quit
      {^Quit(comment: String): end }
    }
) )

In the next example, the fibonacci number is calculated in stead of the factorial, but notice that the user interface process still remains unchanged, except for the cosmetic renaming Fact to Fib.

(nu a : 1=>2:1<Int>;2=>1:2<Int>;Gend)  // Fib Server Protocol
( def Fib() =                          // Define Fib Server
      link(2,a,s,2);                   // Receive Connection
      ( Fib()                          // Start new server
      | s[1] >> x;                     // Receive argument
        if (x=0) or (x=1)              // If simple case
        then s[2] << 1;end             // Return directly
        else link(2,a,t1,1);           // Connect to (another) Fib Server
             link(2,a,t2,1);           // Connect to (a third) Fib Server
             t1[1]<<x-1;               // Send x-1 to second server
             t2[1]<<x-2;               // Send x-2 to third server
             t1[2]>>y1;                // Receive fib(n-1)
             t2[2]>>y2;                // Receive fib(n-2)
             s[2]<<y1+y2;              // Send result: fib(n-1)+fib(n-2)
             end
      )
  in Fib()
| (nu gui: {^Fib: {^Quit: Gend} })      // User Interface Behavior
  ( link(1,gui,user,1);                 // Create User Interface
    guisync(1,user,1)                   // Wait for User Input
    {^Fib(n: Int):                      // Request n
      link(2,a,s,1);                    // Connect to Fib Server
      s[1] << n;                        // Send n
      s[2] >> result;                   // Receive fib(n)
      guivalue(1,user,1,"Fib:",result); // Add result to User Interface
      guisync(1,user,1)                 // Wait for user to quit
      {^Quit(comment: String): end }
    }
) )

Cooperation Example

A screenshot of the three user interfaces implemented in this example
A screenshot of the three user interfaces implemented in this example
  // The Choreography
  // Patient: 1
  // Doctor: 2
  // Nurse: 3
(nu a: { ^Pdata: 1=>2:2<String>;1=>3:3<String>;rec $stateD.
           { ^Pdata: 1=>2:2<String>;1=>3:3<String>;$stateD,
             ^Dschedule: 2=>1:1<String>;2=>3:3<String>;rec $stateDS.
               { ^Pdata: 1=>2:2<String>;1=>3:3<String>;$stateD,
                 ^Dschedule: 2=>1:1<String>;2=>3:3<String>;$stateDS,
                 ^Nschedule: 3=>1:1<String>;3=>2:2<String>;$stateDS,
                 ^Dresult: 2=>1:1<String>;Gend
               },
             ^Nschedule: 3=>1:1<String>;3=>2:2<String>;rec $stateDS.
               { ^Pdata: 1=>2:2<String>;1=>3:3<String>;$stateD,
                 ^Dschedule: 2=>1:1<String>;2=>3:3<String>;$stateDS,
                 ^Nschedule: 3=>1:1<String>;3=>2:2<String>;$stateDS,
                 ^Dresult: 2=>1:1<String>;Gend
               }
           }
       })
( // Patient
  link(3,a,s,1);
  guisync(3,s,1)
  { ^Pdata(symptoms: String):
      guivalue(3,s,1,"symptoms",symptoms);
      s[2]<<symptoms;
      s[3]<<symptoms;
      def StateD(s: rec %stateD.
                    { ^Dschedule: 1>><String>;rec %stateDS.
                        { ^Dresult: 1>><String>;Lend,
                          ^Dschedule: 1>><String>;%stateDS,
                          ^Nschedule: 1>><String>;%stateDS,
                          ^Pdata: 2<<<String>;3<<<String>;%stateD
                        },
                      ^Nschedule: 1>><String>;rec %stateDS.
                        { ^Dresult: 1>><String>;Lend,
                          ^Dschedule: 1>><String>;%stateDS,
                          ^Nschedule: 1>><String>;%stateDS,
                          ^Pdata: 2<<<String>;3<<<String>;%stateD
                        },
                      ^Pdata: 2<<<String>;3<<<String>;%stateD
                    }@(1 of 3)) =
        def StateDS(s: rec %stateDS.
                       { ^Dresult: 1>><String>;Lend,
                         ^Dschedule: 1>><String>;%stateDS,
                         ^Nschedule: 1>><String>;%stateDS,
                         ^Pdata: 2<<<String>;3<<<String>;rec %stateD.
                           { ^Dschedule: 1>><String>;rec %stateDS.
                               { ^Dresult: 1>><String>;Lend,
                                 ^Dschedule: 1>><String>;%stateDS,
                                 ^Nschedule: 1>><String>;%stateDS,
                                 ^Pdata: 2<<<String>;3<<<String>;%stateD
                               },
                             ^Nschedule: 1>><String>;rec %stateDS.
                               { ^Dresult: 1>><String>;Lend,
                                 ^Dschedule: 1>><String>;%stateDS,
                                 ^Nschedule: 1>><String>;%stateDS,
                                 ^Pdata: 2<<<String>;3<<<String>;%stateD
                               },
                             ^Pdata: 2<<<String>;3<<<String>;%stateD
                           }
                       }@(1 of 3)) =
          guisync(3,s,1)
          { ^Pdata(symptoms: String):
              guivalue(3,s,1,"symptoms",symptoms);
              s[2]<<symptoms;
              s[3]<<symptoms;
              StateD(s),
            ^Nschedule():
              s[1]>>schedule;
              guivalue(3,s,1,"schedule",schedule);
              StateDS(s),
            ^Dschedule():
              s[1]>>schedule;
              guivalue(3,s,1,"schedule",schedule);
              StateDS(s),
            ^Dresult():
              s[1]>>result;
              guivalue(3,s,1,"result",result);
              end
          }
        in guisync(3,s,1)
           { ^Pdata(symptoms: String):
               guivalue(3,s,1,"symptoms",symptoms);
               s[2]<<symptoms;
               s[3]<<symptoms;
               StateD(s),
             ^Dschedule():
               s[1]>>schedule;
               guivalue(3,s,1,"schedule",schedule);
               StateDS(s),
             ^Nschedule():
               s[1]>>schedule;
               guivalue(3,s,1,"schedule",schedule);
               StateDS(s)
           }
      in StateD(s)
  }
| // Doctor
  link(3,a,s,2);
  guisync(3,s,2)
  { ^Pdata():
      s[2]>>symptoms;
      guivalue(3,s,2,"symptoms",symptoms);
      def StateD(s: rec %stateD.
                    { ^Dschedule: 1<<<String>;3<<<String>;rec %stateDS.
                        { ^Dresult: 1<<<String>;Lend,
                          ^Dschedule: 1<<<String>;3<<<String>;%stateDS,
                          ^Nschedule: 2>><String>;%stateDS,
                          ^Pdata: 2>><String>;%stateD
                        },
                      ^Nschedule: 2>><String>;rec %stateDS.
                        { ^Dresult: 1<<<String>;Lend,
                          ^Dschedule: 1<<<String>;3<<<String>;%stateDS,
                          ^Nschedule: 2>><String>;%stateDS,
                          ^Pdata: 2>><String>;%stateD
                        },
                      ^Pdata: 2>><String>;%stateD
                    }@(2 of 3)) =
        def StateDS(s: rec %stateDS.
                       { ^Dresult: 1<<<String>;Lend,
                         ^Dschedule: 1<<<String>;3<<<String>;%stateDS,
                         ^Nschedule: 2>><String>;%stateDS,
                         ^Pdata: 2>><String>;rec %stateD.
                           { ^Dschedule: 1<<<String>;3<<<String>;rec %stateDS.
                               { ^Dresult: 1<<<String>;Lend,
                                 ^Dschedule: 1<<<String>;3<<<String>;%stateDS,
                                 ^Nschedule: 2>><String>;%stateDS,
                                 ^Pdata: 2>><String>;%stateD
                               },
                             ^Nschedule: 2>><String>;rec %stateDS.
                               { ^Dresult: 1<<<String>;Lend,
                                 ^Dschedule: 1<<<String>;3<<<String>;%stateDS,
                                 ^Nschedule: 2>><String>;%stateDS,
                                 ^Pdata: 2>><String>;%stateD
                               },
                             ^Pdata: 2>><String>;%stateD
                           }
                       }@(2 of 3)) =
          guisync(3,s,2)
          { ^Pdata():
              s[2]>>symptoms;
              guivalue(3,s,2,"symptoms",symptoms);
              StateD(s),
            ^Nschedule():
              s[2]>>schedule;
              guivalue(3,s,2,"schedule",schedule);
              StateDS(s),
            ^Dschedule(schedule: String):
              guivalue(3,s,2,"schedule",schedule);
              s[1]<<schedule;
              s[3]<<schedule;
              StateDS(s),
            ^Dresult(result: String):
              guivalue(3,s,2,"result",result);
              s[1]<<result;
              end
          }
        in guisync(3,s,2)
           { ^Pdata():
               s[2]>>symptoms;
               guivalue(3,s,2,"symptoms",symptoms);
               StateD(s),
             ^Dschedule(schedule: String):
               guivalue(3,s,2,"schedule",schedule);
               s[1]<<schedule;
               s[3]<<schedule;
               StateDS(s),
             ^Nschedule():
               s[2]>>schedule;
               guivalue(3,s,2,"schedule",schedule);
               StateDS(s)
           }
      in StateD(s)
  }
| // Nurse
  link(3,a,s,3);
  guisync(3,s,3)
  { ^Pdata():
      s[3]>>symptoms;
      guivalue(3,s,3,"symptoms",symptoms);
      def StateD(s: rec %stateD.
                    { ^Dschedule: 3>><String>;rec %stateDS.
                        { ^Dresult: Lend,
                          ^Dschedule: 3>><String>;%stateDS,
                          ^Nschedule: 1<<<String>;2<<<String>;%stateDS,
                          ^Pdata: 3>><String>;%stateD
                        },
                      ^Nschedule: 1<<<String>;2<<<String>;rec %stateDS.
                        { ^Dresult: Lend,
                          ^Dschedule: 3>><String>;%stateDS,
                          ^Nschedule: 1<<<String>;2<<<String>;%stateDS,
                          ^Pdata: 3>><String>;%stateD
                        },
                      ^Pdata: 3>><String>;%stateD
                    }@(3 of 3)) =
        def StateDS(s: rec %stateDS.
                       { ^Dresult: Lend,
                         ^Dschedule: 3>><String>;%stateDS,
                         ^Nschedule: 1<<<String>;2<<<String>;%stateDS,
                         ^Pdata: 3>><String>;rec %stateD.
                           { ^Dschedule: 3>><String>;rec %stateDS.
                               { ^Dresult: Lend,
                                 ^Dschedule: 3>><String>;%stateDS,
                                 ^Nschedule: 1<<<String>;2<<<String>;%stateDS,
                                 ^Pdata: 3>><String>;%stateD
                               },
                             ^Nschedule: 1<<<String>;2<<<String>;rec %stateDS.
                               { ^Dresult: Lend,
                                 ^Dschedule: 3>><String>;%stateDS,
                                 ^Nschedule: 1<<<String>;2<<<String>;%stateDS,
                                 ^Pdata: 3>><String>;%stateD
                               },
                             ^Pdata: 3>><String>;%stateD
                           }
                       }@(3 of 3)) =
          guisync(3,s,3)
          { ^Pdata():
              s[3]>>symptoms;
              guivalue(3,s,3,"symptoms",symptoms);
              StateD(s),
            ^Nschedule(schedule: String):
              guivalue(3,s,3,"schedule",schedule);
              s[1]<<schedule;
              s[2]<<schedule;
              StateDS(s),
            ^Dschedule():
              s[3]>>schedule;
              guivalue(3,s,3,"schedule",schedule);
              StateDS(s),
            ^Dresult():
              end
          }
        in guisync(3,s,3)
           { ^Pdata():
               s[3]>>symptoms;
               guivalue(3,s,3,"symptoms",symptoms);
               StateD(s),
             ^Dschedule():
               s[3]>>schedule;
               guivalue(3,s,3,"schedule",schedule);
               StateDS(s),
             ^Nschedule(schedule: String):
               guivalue(3,s,3,"schedule",schedule);
               s[1]<<schedule;
               s[2]<<schedule;
               StateDS(s)
           }
      in StateD(s)
  }
)
Personal tools