// This file describes the specification language.
// Creataed on July 6, 2011. Updated in July 2012.

// In this document both threads and processes are called processes. 

// The specification describes processes and how they should be coordinated.
// The program implementing the specification consists of a coordinator
// that runs the processes described in the specification and supervises 
// their execution. The coordinator is called supervisor. 

// The specification defines groups of processes. A group may have any number 
// of processes (0, 1, 2, ...). This number may change during the execution of
// the program. The specification determines the initial number of processes 
// in a group and how this number may change. Processes in a group are 
// identical in the sense that they have the same executable code. However, 
// processes in the same group do not have to be in the same stage of 
// execution.  

// A group of processes is implemented by means of executable programs if
// it is defined with the keyword "process". Otherwise, it is implemented 
// by means of threads of the supervisor if it is defined with the keyword
// "thread". 

// The following defines a group or processes

process p1 {

   // The following defines the Petri net representation of the process

    places: p1 p2 p3
    transitions: t0 
    transitions: t1 t2 t3 t4

    // The following describes the arcs connecting places and transitions

    (p1, t0) 
    (p1, t1, p3)

    // A semicolon must be used between instructions on the same row 

    (p3, t4, p1); (t3, p3)

    // The following arc is conditional. The generated program will
    // contain an "if(i >= 1)" instruction before attempting to fire t2. Thus,
    // the variable i must be defined in the context of the C code associated
    // with the place p2.  

    (p2, t2) {i >= 1} 

}

// The following defines a group or processes implemented as threads


thread t1 {

   // The following defines the Petri net representation of the process

    places: p1 p2 p3
    transitions: t1 t2 t3 t4

    // The following describes the arcs connecting places and transitions

    (p1, t1) 
    (p1, t2, p3)
    (p3, t3, p2); (p2, t4, p1); 

}


// The Petri net associated with a supervisor is generated automatically.
// However, the user has the option to specify additional components to be
// included in the Petri net of the supervisor. The following block defines
// such a component.

supervisor sc {
    places: p1 p2
    transitions: t1

    (p1, t1, p2)
}


// The following synchronizes the transition t1 of process p1 with the 
// transition t3 of the process t1. 

sync p1.t1 t1.t3

// Constraints can be described by means of inequalities

2*p1.q.t2 - t1.p3 <= 1 // firing vector element: process.q.transition
                       // marking vector element: process.place

t1.v.t1 <= t1.v.t2  // Parikh vector element: process.v.transition


// The following describes the initial number of processes in each group.
// It also describes the stage in which each process should be started. 

initialize: p1(p1:1, p2:2) 
initialize: t1(p2:1) sc(p1:5)

// The group p1 will have three processes: one starting in p1 and two starting
// in p2. The group t1 will have only one process and that process will start 
// in p2. Now, sc is not a process group but a supervisor component. The 
// initialization of sc requests that the Petri net of sc will have an initial
// marking with 5 tokens in p1. 

// By default, a group of processes is initialized with zero processes. 

// Transitions that should be live can be specified as follows.
// NOTE: Avoid this instruction when possible, since the synthesis of a 
// deadlock prevention policy is computationally intensive and can take much 
// time.  

live: t1.t2 // the supervisor should ensure that the transition t2 of the 
            // process group t1 is live.


// The following blocks are OPTIONAL.

// A segment of code can be associated with each place. The following 
// instruction defines the code of the place p3 of the process p1.

p1.p3 {
   i = i + 1;
   j = 10*i;
}

// If several transitions could be fired from a place (that is, their
// conditions, if any, are satisfied and the supervisor could fire any of them)
// the next transition will be selected randomly. However, if the programmer
// defines a "select function" and assigns it to the place, the fired 
// transition will be determined by the select function. Thus, conditions
// labeling a transition are implemented only if no select function is defined.
// The following line requests that p1_select() be called in order to 
// determine the transition that should be fired from the place p1 of the 
// process p1. Note the requirements on the select function below. 

p1.p1.select { p1_select(___TR); /* ___TR: defined in context of call */ } 

// Requirements on the select function:
// - It must return the number of transitions written to ___TR.
// - The select function should write to ___TR[0], ___TR[1], ...
//   the ___TRData element of the selected transitions, in the order 
//   of preference. See the definition of the p1_select function in this file.
// - The parameters of the function may be arbitrary.
// - The code generator will write:
//   ___i = [select function call]
//   where [select function call] stands for whatever is written between 
//   braces in the select command. For instance, the select command  above  
//   is implemented as
//   ___i = p1_select(___TR); /* ___TR: defined in context of call */


// Any instructions that a process should execute when it is started
// can be specified by means of a main block

p1.main {
   i = 0;
   j = 1;
}

// Header files and other definitions that should appear in the source file of 
// a process can be specified by means of an include block

p1.include {
   #include"string.h"
   #define MAX 10

   int i, j;

   struct myarray { int i; float k; };

   static struct myarray array[MAX];

   static int p1_select(struct ___trans* ___TR) {
     // Selects the transitions 0 and 1 and gives precedence to transition 1.
     ___TR[0] = ___TRData[1]; ___TR[1] = ___TRData[0];
     return 2; // returns the number of entries written to ___TR
   }
}

// Instructions on how to build the executable file associated with a process
// can be specified in a build block. Note that the software will replace $$$ 
// with the name of the file defining the process (without extension). 

p1.build { gcc -g -o $$$.exe $$$.c }

// Copies of a process group can be specified as follows

p1c = p1 // p1c is another process group

// Note that p1 has been defined with the keyword 'process'. Thus, p1c will
// also be of the type 'process'. If the copy should have a different type,
// the desired type should be stated before the assignment. 

thread p1c2 = p1

// On the line above, p1c2 is defined as a copy of p1 of the type 'thread'.

// Instructions that the supervisor should execute when it is started 
// can be specified by means of a main block

main {
   fprintf(stdout, "The supervisor is starting ...");
}

// An include block can also be defined for the supervisor

include {
   #define MAX_INP 3
   #include"ctype.h"
}


// The build block of the supervisor can be used to specify additional 
// command line parameters that should be used when building the program

build { -I. }
