[Pntool-developers] SF.net SVN: pntool:[247] spnbox

[<mio...@us...>]

Revision: 247
          http://pntool.svn.sourceforge.net/pntool/?rev=247&view=rev
Author:   miordache
Date:     2011-05-11 12:20:38 +0000 (Wed, 11 May 2011)

Log Message:
-----------


Modified Paths:
--------------
    newcodegen/ProcessTemplate.c
    newcodegen/SupervisorTemplate.c
    newcodegen/plantCompiler.c
    pnheaders/Makefile
    pnheaders/main_function.c
    pnheaders/matrix.c
    pnheaders/matrix.h
    pnheaders/pns.c
    pnheaders/pns.h
    spnbox/linenf.c
    spnbox/spnbox.h

Modified: newcodegen/ProcessTemplate.c
===================================================================
--- newcodegen/ProcessTemplate.c	2011-04-08 22:36:44 UTC (rev 246)
+++ newcodegen/ProcessTemplate.c	2011-05-11 12:20:38 UTC (rev 247)
@@ -88,6 +88,8 @@
 
   ___send_exit_notification(___pthr);
 
+  if(p___) free(p___);
+
   debugInfo("The end of the main function was reached");
 
   return 0;

Modified: newcodegen/SupervisorTemplate.c
===================================================================
--- newcodegen/SupervisorTemplate.c	2011-04-08 22:36:44 UTC (rev 246)
+++ newcodegen/SupervisorTemplate.c	2011-05-11 12:20:38 UTC (rev 247)
@@ -314,7 +314,7 @@
     for(___ptl = ___pr->tlist, ___i = 0; ___i < ___pr->ntlist; ___i++) 
       if(___t == ___ptl[___i].t)
 	break;
-    if(___ptl) { // That is, if the transition was found
+    if(___i < ___pr->ntlist) { // That is, if the transition was found
       ___pr->fireable = ___t;
       ___pr->atype |= 2; // set the bit 1
       ___qlast->next_in_qelist = ___pr;
@@ -1060,14 +1060,21 @@
       ___a = IsPermissible(___p); // creates EntryList (qelist)
       if(___a > 0) { // then the request of ___p can be resolved
 
+	// Make sure that ___pn is not in EntryList, since everything in
+	// EntryList will be removed from the queue
+
+	for(; ___pn; ___pn = ___pn->next_in_queue)
+	  if(!(___pn->atype & 2)) // if not in EntryList
+	    break;
+
 	// Grant permission to fire to the processes in EntryList
 	// Remove also from queue and wait list processes in EntryList
 
 	for(___pa = ___p; ___pa; ___pa = ___pa->next_in_qelist) {
 	  // This loop does not affect 'qelist' (EntryList).
-	  // However, it does affect 'queue' and 'wtlist'. 
-	  if(___pn == ___pa) // if ___pn will be removed from queued requests
-	    ___pn = ___pn->next_in_queue; // select next queued request
+	  // However, it does affect 'queue' and 'wtlist'.
+	  //if(___pn == ___pa) // if ___pn will be removed from queued requests
+	  //  ___pn = ___pn->next_in_queue; // select next queued request
 	  ___send_permission_msg(___pa);
 	  ___remove_from_queue(___pa); // remove ___pa from queued requests
 	  ___remove_from_wtlist(___pa);

Modified: newcodegen/plantCompiler.c
===================================================================
--- newcodegen/plantCompiler.c	2011-04-08 22:36:44 UTC (rev 246)
+++ newcodegen/plantCompiler.c	2011-05-11 12:20:38 UTC (rev 247)
@@ -199,6 +199,7 @@
     if(procArray[i]->thread) fprintf(plantFile,"\n#define ___THREAD\n");
     else fprintf(plantFile,"\n#define ___PROCESS\n");
     fprintf(plantFile,"#define ___NAME \"%s\"\n", procArray[i]->name);
+    fprintf(plantFile,"#define ___INSTANCE \"%s\"\n", procArray[i]->instance);
         
     // generate declarations/definitions
     incl = genDefineBlock(procArray[i], TrInfo[i]); 

Modified: pnheaders/Makefile
===================================================================
--- pnheaders/Makefile	2011-04-08 22:36:44 UTC (rev 246)
+++ pnheaders/Makefile	2011-05-11 12:20:38 UTC (rev 247)
@@ -1,4 +1,4 @@
-COMPILER=gcc -g
+COMPILER=gcc -g -I../spnbox
 
 generate: general.o matrix.o pns.o insert.o
 

Modified: pnheaders/main_function.c
===================================================================
--- pnheaders/main_function.c	2011-04-08 22:36:44 UTC (rev 246)
+++ pnheaders/main_function.c	2011-05-11 12:20:38 UTC (rev 247)
@@ -7,6 +7,9 @@
 
 int inline is_verbose() { return verb; }
 
+
+
+
 void br_filter(char *p) {  // removes beginning and end braces
   int n;
   if(!p)
@@ -31,16 +34,17 @@
   return ! p[i];
 }
 
-int th_filter(char** ap) { // filters <thread> commands
+int th_filter(char** ap, char* pattern) { // remove pattern from strings
   char* p = *ap, *p2 = 0;
-  int i;
-  if(!p) return 0;
+  int i, n;
+  if(!p || !pattern) return 0;
+  n = strlen(pattern);
   for(i = 0; p[i]; i++) {
     if(p[i] == ' ' || p[i] == '\t')
       continue;
-    if(!strncmp(p+i, "<thread>", 8)) {
-      if(!is_empty(p+i+8)) // else p2 remains equal to zero
-        asprintf(&p2, "%s", p+i+8); 
+    if(!strncmp(p+i, pattern, n)) {
+      if(!is_empty(p+i+n)) // else p2 remains equal to zero
+        asprintf(&p2, "%s", p+i+n); 
       free(*ap);
       *ap = p2;
       return 1;
@@ -66,8 +70,15 @@
       continue;
     br_filter(sp->process_array[i]->build);
     br_filter(sp->process_array[i]->include);
-    if(th_filter(&(sp->process_array[i]->build)))
-      sp->process_array[i]->thread = 1;
+    //if(th_filter(&(sp->process_array[i]->build))) 
+    //sp->process_array[i]->thread = 1;
+
+    // Is this a thread?
+    sp->process_array[i]->thread = th_filter(&(sp->process_array[i]->build),\
+					     "<thread>");
+    // Is this a supervisor component?
+    sp->process_array[i]->supervisor=th_filter(&(sp->process_array[i]->build),\
+					     "<supervisor>");
     pn = sp->process_array[i]->pn; 
     if(pn) {
       if(pn->segment) 
@@ -87,23 +98,28 @@
 
 int main(int na, char* argv[]) {
 
-  int i, j, l1, l2, UCcnt, UOcnt, *Tuc, *Tuo, *UClst, *UOlst;
-  int labelcount = 0, finish = 0;
+  int i, j, l1, l2, UCcnt, UOcnt, LVcnt, *Tuc, *Tuo, *Tlive, *UClst, *UOlst, *LVlst;
+  int labelcount = 0, finish = 0, plcnum, spcnum;
   char* input, *build;
   FILE* f;
   specs *sp;
   syncc *snc;
-  pns pn, *apnsv;
+  pns pn, pn1, *apnsv;
+  process **plant_array, **spv_array;
   matrix L, C, H;
   int *B;
   struct myinsert ins;
-  linenf_r lin_res;
+  linenf_r lin_res, lin_res2;
+  dp_p LVparams;
+  dp_r LVresult;
   struct synclist *syncl, *syncl2;
   struct sync_element *syn_el, *syn_el2;
   struct label_lst* lls;
   TrData** TInf;
 
 
+  // 1. INITIALIZATION
+
   ins = InitInsert(512); // used to store command line parameters 
   verb = 0;
   input = 0;
@@ -168,11 +184,15 @@
     return 0;
   }
 
-  // Call the translator
+  // 2. TRANSLATE SPECIFICATION
 
   sp = ScanInput(input);
-  if(!sp)  // check translator result
+
+  // 2.1. Check translator result
+
+  if(!sp)  
     return 1;
+
   if(sp->process_num <= 0) {
     fprintf(stderr, "No processes defined! Nothing to do.\n");
     dealloc_specs(sp);
@@ -180,23 +200,40 @@
     return 0; 
   }
 
-  sp_filter(sp); // remove extra braces
+  sp_filter(sp); // detect settings and remove extra braces
 
   if(is_verbose() >= 3) { // For debugging
     for(i = 0; i < sp->process_num; i++) {
       printf("\n\n======================================================");
-      printf("\nPROCESS NAME: %s\n", sp->process_array[i]->name);
+      if(sp->process_array[i]->supervisor)
+	printf("\nSUPERVISOR COMPONENT: ");
+      else if(sp->process_array[i]->thread)
+	printf("\nTHREAD NAME: ");
+      else
+	printf("\nPROCESS NAME: ");
+      printf("%s (%s)\n", sp->process_array[i]->instance, sp->process_array[i]->name);
       displaypn(*(sp->process_array[i]->pn), stdout);
     }
   }
 
+  for(i = 0; i < sp->process_num; i++)
+    if(!sp->process_array[i]->supervisor)
+      break;
 
-  // Label the PNs
+  if(i >= sp->process_num) {
+    fprintf(stderr, "No plant components defined! Nothing to do.\n");
+    dealloc_specs(sp);
+    if(build) free(build);
+    return 0; 
+  }
 
+
+  // 2.2 Label the PNs
+
   for(i = 0; i < sp->process_num; i++) 
     updatepn(sp->process_array[i]->pn, "freelabel", &labelcount);
   
-  // Deal with synchronization constraints
+  // 2.2.1 Deal with synchronization constraints
 
   for(i = 1; i; ) /* i = 0 indicates when loop may end */
     for(i = 0, snc = sp->synclist; snc; snc = snc->next) {
@@ -208,7 +245,7 @@
       }
     }
 
-  // Obtain SC specification. Currently:
+  // 2.3 Obtain SC specification. Currently:
   // extract the L, C, H, and b matrices (more complex specs to be done later)
 
   extractLHCB(sp, &pn, &L, &H, &C, &B);
@@ -219,18 +256,23 @@
     printLHCB(&pn, &L, &H, &C, B, -1, stdout);
   }
 
-  // Perform SC
+  // 3. SUPERVISORY CONTROL
 
+  // 3.1 Enforce SC specs (linear constraints supported currently)
+
   Tuc = tcalloc(pn.tnum, sizeof(*Tuc));
   Tuo = tcalloc(pn.tnum, sizeof(*Tuo));
+  Tlive = tcalloc(pn.tnum, sizeof(*Tlive));
   if(pn.t)
     for(i = 0; i < pn.tnum; i++) {
       Tuc[i] = pn.t[i].uncontrollable;
       Tuo[i] = pn.t[i].unobservable;
+      Tlive[i] = pn.t[i].live;
     }
 
   UCcnt = findIndices(Tuc, pn.tnum, sizeof(*Tuc), &UClst);
   UOcnt = findIndices(Tuo, pn.tnum, sizeof(*Tuo), &UOlst);
+  LVcnt = findIndices(Tlive, pn.tnum, sizeof(*Tlive), &LVlst);
 
   lin_res = linenf(&pn.out, &pn.in, &L, B, pn.marking, &H, &C, \
 		   UCcnt, UClst, UOcnt, UOlst);
@@ -241,64 +283,178 @@
     printLHCB(&pn, &lin_res.Lf, 0, &lin_res.Cf, lin_res.bf, -1, stdout);
   }
 
-  free(Tuc); free(Tuo); free(UClst); free(UOlst);
-
   // Check whether SC was successful
 
   if(strcmp(lin_res.how, "OK"))
     merror(0, "MAIN FUNCTION: SC has failed. Relax the specification\n\
     such as by reducing the number of uncontrollable and unobservable transitions");
 
-  // Enforce liveness
+  // 3.2. Enforce liveness
 
-     // no liveness enforcement at this time
+  // - Liveness enforcement is applied to the closed-loop
+  // - Check whether the initial marking satisfies the constraints. 
+  // - The result of liveness enforcement is enforced on the closed-loop
+  //   with linenf and no uncontro. and unobs. transitions, since the result
+  //   is guaranteed to be admissible. 
+  // - The supervisor is extracted from the closed-loop reported by linenf via
+  //   getSupervisor
 
-  // Extract supervisor as a pn
+  // For future work: 
+  // - calculate initial marking constraints: check marking constraints satisfied by initial marking of plant.
+  // - check if responsiveness is guaranteed.
+  // - To help convergence, invariants from previous constraints should be 
+  //   communicated by means of the L, B parameters of the function dp. 
 
+
+  if(LVcnt) { // If T-liveness enforcement has been requested
+    if(is_verbose() >= 3) { // For debugging
+      printf("\n\n======================================================");
+      printf("\n\nLiveness enforcement has been requested. This may take a while ...\n");
+    }
+    // Initialize parameters
+    memset(&LVparams, 0, sizeof(LVparams));
+    LVparams.Dm = lin_res.Dfm; LVparams.Dp = lin_res.Dfp;
+    LVparams.Tuc = UClst; LVparams.TucCount = UCcnt;
+    LVparams.Tuo = UOlst; LVparams.TuoCount = UOcnt;
+    LVparams.IncludeT = LVlst; LVparams.IncludeCount = LVcnt;
+    LVparams.option = 12 + (is_verbose() >= 4);
+
+    LVresult = dp(&LVparams); // apply the T-liveness enforcement procedure
+    if(strcmp(LVresult.how, "OK"))
+      merror(0, "MAIN FUNCTION: Liveness enforcement has failed. Relax the specification\nsuch as by reducing the number of uncontrollable and unobservable transitions.\nSee also the log file of the liveness enforcement algorithm.");
+
+    // Verify L*m0 >= B
+    if(!TestLCB(&LVresult.Lf, lin_res.ms0, 0,0, GREATER_OR_EQUAL, LVresult.Bf))
+      merror(0, "MAIN FUNCTION: Liveness enforcement has failed due to insufficient initial \nmarking (the initial marking does not satisfy the L*m >= B constraints). \nRelax the specification such as by increasing the initial marking and \nreducing the number of uncontrollable and unobservable transitions. See also \nthe log file of the liveness enforcement algorithm.");
+
+    // Verify L0*m0 >= b0
+    if(!TestLCB(&LVresult.L0f, lin_res.ms0,0,0,GREATER_OR_EQUAL, LVresult.B0f))
+      merror(0, "MAIN FUNCTION: Liveness enforcement has failed due to insufficient initial \nmarking (the initial marking does not satisfy the L0*m >= B0 constraints). \nRelax the specification such as by increasing the initial marking and \nreducing the number of uncontrollable and unobservable transitions. See also \nthe log file of the liveness enforcement algorithm.");
+
+    // Convert L*m >= B to L*m <= B (the input expected by linenf)
+    InvertSignOfMatrix(&LVresult.Lf); // L = -L
+    InvertSignOfVector(LVresult.Bf, NumberOfRows(LVresult.Lf)); // B = -B
+
+    lin_res2 = linenf(&lin_res.Dfm, &lin_res.Dfp, &LVresult.Lf, LVresult.Bf,\
+		      lin_res.ms0, 0, 0, 0, 0, 0, 0); 
+    // no uncontr. and unobs. transitions have to be passed to linenf 
+    // since constraints are admissible
+
+    DeallocateDp(&LVresult); DeallocateLinenf(&lin_res);
+
+    lin_res = lin_res2;
+  }
+
+  free(Tuc); free(Tuo); free(Tlive); free(UClst); free(UOlst); free(LVlst);
+
+  // 3.3 Extract supervisor as a pn
+
   apnsv = getSupervisor(&pn, &lin_res.Dfm, &lin_res.Dfp, lin_res.ms0);
 
   if(is_verbose() >= 3) { // For debugging
     printf("\n\n======================================================");
-    printf("\nCOMPOSED PN\n");
+    printf("\nCOMPOSED PLANT PN PLUS PREDEFINED SUPERVISOR COMPONENTS\n");
     displaypn(pn, stdout);
     printf("\n\n======================================================");
     if(apnsv) {
-      printf("\nSUPERVISOR PN\n");
+      printf("\nSC GENERATED SUPERVISOR\n");
       displaypn(*apnsv, stdout);
     }
     else
-      printf("\nNO SUPERVISOR PN\n");
+      printf("\nNO SC GENERATED SUPERVISOR\n");
   }
   deallocpn(&pn);
 
-  // need functions to free linenf_r structures and similar structures
 
-  // Generate code
+  // 4. GENERATE CODE
 
+  // 4.1 Separate supervisor components from plant components 
 
+  spv_array = tcalloc(sp->process_num, sizeof(*spv_array));
+  plant_array = tcalloc(sp->process_num, sizeof(*plant_array));
+  for(i = 0, plcnum = 0, spcnum = 0; i < sp->process_num; i++) {
+    if(sp->process_array[i]->supervisor) {
+      spv_array[spcnum] = sp->process_array[i];
+      spcnum++;
+    }
+    else {
+      plant_array[plcnum] = sp->process_array[i];
+      plcnum++;
+    }
+  }
 
-  // Obtain also a synclist structure with the sync data
+  // 4.2 Compose supervisor components with SC generated supervisor. 
+
+  pn = pn_composition(spv_array, spcnum);
+  pn1 = composepn(apnsv, &pn);
+  if(apnsv)
+    free(apnsv);
+  deallocpn(&pn); // free intermediary result
+  apnsv = &pn1;
+
+  if(is_verbose() >= 3 && spcnum) { 
+    // If spcnum != 0, then SC supervisor and final supervisor are different. 
+    printf("\n\n======================================================");
+    if(apnsv) {
+      printf("\nFINAL SUPERVISOR\n");
+      displaypn(*apnsv, stdout);
+    }
+  }
+
+  // 4.3 Obtain a synclist structure with the sync data for plant processes
+
+  /* May be deleted after testing the change
   lls = get_label_list(sp->process_array, sp->process_num);
   syncl = get_synclist(lls, sp->process_array);
   TInf = get_TrData(apnsv, sp->process_array, sp->process_num, lls);
+  */
 
-  //exit(1);
+  lls = get_label_list(plant_array, plcnum);
+  syncl = get_synclist(lls, plant_array);
+  TInf = get_TrData(apnsv, plant_array, plcnum, lls);
 
-  CodeGenerator(apnsv, sp->name, sp->process_array, sp->process_num,\
+  // Call the code generation function
+
+  /*CodeGenerator(apnsv, sp->name, sp->process_array, sp->process_num,	\
 		  syncl, TInf, build); 
+  */
 
-  // Free memory
+  CodeGenerator(apnsv, sp->name, plant_array, plcnum, syncl, TInf, build);
 
+
+  // 5. TERMINATE
+
   if(apnsv) {
     deallocpn(apnsv);
-    free(apnsv);
+    //free(apnsv);
   }
+  free(plant_array);
+  free(spv_array);
   dealloc_specs(sp);
   if(build) free(build);
   free_label_list(lls);
   free_synclist(syncl);
-  free_TrData(TInf, sp->process_num);
+  free_TrData(TInf, plcnum);
 
   return 0;
 }
 
+
+
+/* Future improvements for deadlock prevention.
+
+   Currently deadlock prevention does not account for determinism. Thus, 
+   some potential deadlocks may remain undetected. 
+
+   The following function could be defined in the future to help the deadlock 
+   prevention procedure converge. Additionally, a function for initial 
+   markings could be developed.
+
+matrix getLB(matrix Lf, matrix Cf, int *Bf, int** B) {
+  // Outputs a matrix L such that L*m <= B contains the rows of 
+  // Lf*m + Cf*v <= Bf on which Cf is zero. B is also allocated and 
+  // initialized. 
+
+}
+
+*/

Modified: pnheaders/matrix.c
===================================================================
--- pnheaders/matrix.c	2011-04-08 22:36:44 UTC (rev 246)
+++ pnheaders/matrix.c	2011-05-11 12:20:38 UTC (rev 247)
@@ -452,6 +452,89 @@
 
 
 
+inline int TestCondition(int v, int type, int w) {
+/* Checks whether 'v' and 'w' (in this order) are in the relationship 
+   described by 'type', where 'type' may have one of the values in the 
+   range GREATER, ..., LESS. If the relationship is satisfied, the 
+   function returns 1. Else, it returns 0. */
+
+  int a, b;
+
+  if(type < 0) {
+    type = -type;
+    a = v;
+    b = w;
+  }
+  else {
+    a = w;
+    b = v;
+  }
+  switch(type) {
+  case GREATER:
+    if(a >= b)
+      return 0;
+    break;
+  case GREATER_OR_EQUAL:
+    if(a > b)
+      return 0;
+    break;
+  case EQUAL:
+    if(a != b)
+      return 0;
+    break;
+  default:
+    return 0;
+  }
+  return 1;
+}
+
+int TestExpression(const int* v, int c, const int* w, int len) {
+/*  The vectors 'v' and 'w' are compared for the first 'len' elements.
+    'c' may have one of the values in the range GREATER, ..., LESS. 
+    The return value is as follows:
+    * If 'len' <= 0 or v = 0 or w = 0 the function returns a nonzero value;
+    * Else if 'c' is none of the above, the function returns zero;
+    * Else if the expression is satisfied for each pair of elements v[i] and 
+      w[i], the function returns a nonzero value;
+    * Else the function returns zero. */
+
+  const int *a, *b;
+  int i;
+
+  if(!v || !w || len <= 0)
+    return 1;
+  if(c < 0) {
+    a = v;
+    b = w;
+    c = -c;
+  }
+  else {
+    a = w;
+    b = v;
+  }
+  switch(c) {
+  case GREATER:
+    for(i = 0; i < len; i++)
+      if(a[i] >= b[i])
+	return 0;
+    break;
+  case GREATER_OR_EQUAL:
+    for(i = 0; i < len; i++)
+      if(a[i] > b[i])
+	return 0;
+    break;
+  case EQUAL:
+    for(i = 0; i < len; i++)
+      if(a[i] != b[i])
+	return 0;
+    break;
+  default:
+    return 0;
+  }
+  return 1;
+}
+
+
 void free2Darray(int** ar, int nr) {
 /* Used to deallocate an array created with matrix2array or vector2array; nr is the number of rows */
 
@@ -501,7 +584,23 @@
   memset(m, 0, sizeof(*m));
 }
 
+inline void InvertSignOfMatrix(matrix* m) {
+  int i, j, r, n;
+  if(!m) return;
+  r = NumberOfRows(*m);
+  n = NumberOfColumns(*m);
+  for(i = 0; i < r; i++)
+    for(j = 0; j < n; j++)
+      SetMatrixEl(m, i, j, -GetMatrixEl(m, i, j)); 
+}
 
+inline void InvertSignOfVector(int* v, int len) {
+  int i;
+  if(!v) return;
+  for(i = 0; i < len; i++)
+    v[i] = -v[i];
+}
+
 /* To do:
     - _setmatrel3 does not deallocate elements set to zero
     - consider better matrix representations. For instance, for type 3 

Modified: pnheaders/matrix.h
===================================================================
--- pnheaders/matrix.h	2011-04-08 22:36:44 UTC (rev 246)
+++ pnheaders/matrix.h	2011-05-11 12:20:38 UTC (rev 247)
@@ -127,6 +127,9 @@
 int** matrix2array(matrix m); 
 /* Converts a matrix object to an array of integers: result[i][j] = elem(i,j)*/
 
+void free2Darray(int** ar, int nr);
+/* Use to deallocate an array created with matrix2array or vector2array; nr is the number of rows */
+
 int findIndices(void* vect, int n, int esize, int** answer );
 /* Finds the indices of the nonzero elements of 'vect'. Here, 'vect' is a 
    vector of 'n' elements. Each element of 'vect' has the size 'esize'. The
@@ -137,7 +140,35 @@
    This function is similar to the find function of Matlab. */
 
 
-void free2Darray(int** ar, int nr);
-/* Use to deallocate an array created with matrix2array or vector2array; nr is the number of rows */
+// Changes in the following can affect TestCondition and TestExpression !
+#define GREATER 2
+#define GREATER_OR_EQUAL 1
+#define EQUAL 0
+#define LESS_OR_EQUAL -1
+#define LESS -2
 
+inline int TestCondition(int v, int type, int w);
+/* Checks whether 'v' and 'w' (in this order) are in the relationship 
+   described by 'type', where 'type' may have one of the values in the 
+   range GREATER, ..., LESS. If the relationship is satisfied, the 
+   function returns 1. Else, it returns 0. */
+
+int TestExpression(const int* v, int c, const int* w, int len);
+/*  The vectors 'v' and 'w' are compared for the first 'len' elements.
+    'c' may have one of the values in the range GREATER, ..., LESS above. 
+    The return value is as follows:
+    * If 'len' <= 0 or v = 0 or w = 0 the function returns a nonzero value;
+    * Else if 'c' is none of the above, the function returns zero;
+    * Else if the expression is satisfied for each pair of elements v[i] and 
+      w[i], the function returns a nonzero value;
+    * Else the function returns zero. */
+
+inline void InvertSignOfMatrix(matrix* m); /* m = -m */
+
+inline void InvertSignOfVector(int* v, int len); /* v = -v */
+
+
+// matrixmath.h and extendedmatrix.h of spnbox have additional matrix functions
+
+
 #endif

Modified: pnheaders/pns.c
===================================================================
--- pnheaders/pns.c	2011-04-08 22:36:44 UTC (rev 246)
+++ pnheaders/pns.c	2011-05-11 12:20:38 UTC (rev 247)
@@ -4,8 +4,8 @@
 ****************************************************************************/
 
 #include"pns.h"
+#include"matrixmath.h"
 
-
 void d2dd(const matrix* D, matrix* Dm, matrix* Dp) {
   int i, j, nr, nc;
   mtype x;
@@ -525,41 +525,18 @@
 
 
 
-pns copypn(pns *src) {
-  pns dst;
+inline pns _copytrans(pns dst, pns *src) {
+  /* This is a subroutine of copypn and composepn for copying transitions
+     and arcs from src to dst. */
+
+  int i;
   arcs *pa; const arcs *pb;
   struct placelist *pd; const struct placelist *ps;
-  int i;
 
-  dst = createpn("pnum tnum mDm mDp", src->pnum, src->tnum, src->out, src->in);
-  if(src->marking)  updatepn(&dst, "m0", src->marking);
-  if(src->C)        updatepn(&dst, "C", src->C);
-  if(src->place_name) 
-    for(i = 0; i < src->pnum; i++)
-      if(src->place_name[i])
-	updatepn(&dst, "place_name", i, src->place_name[i]);
-  if(src->segment)
-    for(i = 0; i < src->pnum; i++)
-      if(src->segment[i])
-	updatepn(&dst, "segment", i, src->segment[i]);
-  if(src->select)
-    for(i = 0; i < src->pnum; i++)
-      if(src->select[i])
-	updatepn(&dst, "select", i, src->select[i]);
-  if(src->trans_name)
-    for(i = 0; i < src->tnum; i++)
-      if(src->trans_name[i])
-	updatepn(&dst, "trans_name", i, src->trans_name[i]);
   if(src->t) {
-    dst.t = tcalloc(dst.tnum, sizeof(src->t[0]));
-    for(i = 0; i < src->tnum; i++)
-      dst.t[i] = src->t[i];
+    dst.t = tcalloc(src->tnum, sizeof(src->t[0]));
+    memcpy(dst.t, src->t, (src->tnum)*sizeof(src->t[0]));
   }
-  if(src->p) {
-    dst.p = tcalloc(dst.pnum, sizeof(src->p[0]));
-    for(i = 0; i < src->pnum; i++)
-      dst.p[i] = src->p[i];
-  }
   if(src->arc_list) { /* copy the list of arcs */
     dst.arc_list = tcalloc(dst.tnum, sizeof(*(dst.arc_list)));
     for(i = 0; i < src->tnum; i++) {
@@ -592,7 +569,39 @@
 }
 
 
+pns copypn(pns *src) {
+  pns dst;
+  int i;
 
+  dst = createpn("pnum tnum mDm mDp", src->pnum, src->tnum, src->out, src->in);
+  if(src->marking)  updatepn(&dst, "m0", src->marking);
+  if(src->C)        updatepn(&dst, "C", src->C);
+  if(src->place_name) 
+    for(i = 0; i < src->pnum; i++)
+      if(src->place_name[i])
+	updatepn(&dst, "place_name", i, src->place_name[i]);
+  if(src->segment)
+    for(i = 0; i < src->pnum; i++)
+      if(src->segment[i])
+	updatepn(&dst, "segment", i, src->segment[i]);
+  if(src->select)
+    for(i = 0; i < src->pnum; i++)
+      if(src->select[i])
+	updatepn(&dst, "select", i, src->select[i]);
+  if(src->trans_name)
+    for(i = 0; i < src->tnum; i++)
+      if(src->trans_name[i])
+	updatepn(&dst, "trans_name", i, src->trans_name[i]);
+  if(src->p) {
+    dst.p = tcalloc(dst.pnum, sizeof(src->p[0]));
+    for(i = 0; i < src->pnum; i++)
+      dst.p[i] = src->p[i];
+  }
+  return _copytrans(dst, src);
+}
+
+
+
 void deallocpn(pns *pn) {
   int i, pnum, tnum;
   pnum = pn->pnum;
@@ -812,17 +821,21 @@
   /* Next we deal with the case when pn1 or pn2 does not have transitions */
 
   if(!nt1 || !nt2) {
-    if(!nt1) { /* if pn1 does not have transitions */
-      if(pn2->t) { /* if pn2 has transitions and transition information */
-	pn.t = tcalloc(pn.tnum,sizeof(pn.t[0]));
-	memcpy(pn.t, pn2->t, nt2*sizeof(pn.t[0])); /* copy info */
-      }
-    }
+    if(!nt1)  /* if pn1 does not have transitions */
+      pn = _copytrans(pn, pn2); // copies transitions and trans arcs to pn
     else /* if pn2 does not have transitions */
-      if(pn1->t) { /* if pn1 has transitions and transition information */
-	pn.t = tcalloc(pn.tnum,sizeof(pn.t[0]));
-	memcpy(pn.t, pn1->t, nt1*sizeof(pn.t[0])); /* copy info */
+      pn = _copytrans(pn, pn1);
+    // Copy also input/output matrix elements
+    for(j = 0; j < nt1; j++) 
+      if(np1) {
+	Copy2ZeroColumn(&(pn1->in),j,&(pn.in),j,0);
+	Copy2ZeroColumn(&(pn1->out),j,&(pn.out),j,0);
       }
+    for(j = 0; j < nt2; j++) 
+      if(np2) {
+	Copy2ZeroColumn(&(pn2->in),j,&(pn.in),j,np1);
+	Copy2ZeroColumn(&(pn2->out),j,&(pn.out),j,np1);
+      }
     return pn;
   }
 
@@ -910,6 +923,34 @@
 }
 
 
+
+pns pn_composition(process** process_array, int num) {
+  /* Composes the PNs in the process array and returns the result. */
+  pns pn, pn1, *apn;
+  int i;
+
+  if(num <= 0 || !process_array) 
+    memset(&pn, 0, sizeof(pn)); // return null pn
+  else if(num == 1)
+    pn = copypn(process_array[0]->pn);
+  else {
+    apn = process_array[0]->pn;
+    for(i = 1; i < num; i++) {
+      if(i > 1) {
+	pn1 = pn; // save intermediary result for subsequent deallocation
+	apn = &pn1;
+      }
+      pn = composepn(apn, process_array[i]->pn);
+      if(i > 1)
+        deallocpn(&pn1); // free intermediary result
+    }
+  }
+
+  return pn;
+}
+
+
+
 int isfreelabeled(pns *rpn) {
   int i, j, label;
 
@@ -1175,9 +1216,9 @@
 /* This is a temporary implementation; future work should take in account that
    sp can contain more general specifications */
 
-/* The implementation assumes that each pn is free labeled and that no disjunctive 
-   constraints are present. */
+/* The implementation assumes that no disjunctive constraints are present. */
 
+
 int find_var_index(variable* var, pns* pn, specs* sp) {
   int i, k;
   int lab;
@@ -1199,7 +1240,7 @@
       merror(0, "EXTRACTLHCB: index %d >= tran. number (%d)", var->index, var->pn->tnum);
     lab = var->pn->t[var->index].l;
     for(i = 0; i < pn->tnum; i++)
-      if(pn->t[i].l == lab)
+      if(pn->t[i].l == lab) // Assumes free-labeled PN
 	return i;
     merror(0, "EXTRACTLHCB: Variable does not match specified PNs");
   }
@@ -1215,6 +1256,9 @@
 
   /* Find the composed PN */
 
+  *pn = pn_composition(sp->process_array, sp->process_num);
+
+  /* May be deleted after testing pn_composition above
   if(sp->process_num == 1)
     *pn = copypn(sp->process_array[0]->pn);
   else {
@@ -1229,6 +1273,7 @@
         deallocpn(&pn1); // dealloc intermediary result
     }
   }
+  */
 
   /* Find cnum, the number of constraints */
   for(c = sp->constraint_list, cnum = 0; c; c = c->next, cnum++);
@@ -1238,7 +1283,10 @@
   AllocateMatrixType(3, L, cnum, pn->pnum);
   AllocateMatrixType(3, H, cnum, pn->tnum);
   AllocateMatrixType(3, C, cnum, pn->tnum);
-  *B = tcalloc(cnum, sizeof(**B));
+  if(!cnum)
+    *B = 0;
+  else
+    *B = tcalloc(cnum, sizeof(**B));
 
   /* Initialize L, H, C, B */
 
@@ -1361,6 +1409,55 @@
 }
 
 /***************************************************************************
+ TestLCB
+****************************************************************************/
+
+int TestLCB(matrix* L, int* m, matrix* C, int* v, int type, int* B) {
+
+/* 'type' should be GREATER, LESS, EQUAL, GREATER_OR_EQUAL, or LESS_OR_EQUAL
+   (which are defined in matrix.h).
+
+   The function calculates L*m + C*v and compares the result to B.
+   If all elements of the result satisfy the 'type' constraint when compared
+   to B, then the function returns 1. Otherwise, it returns zero. 
+
+   Unused entries may be set to zero. For instance, TestLCB(L,m,0,0,LESS,B,n)
+   checks whether L*m < B. */ 
+
+  int i, a, n;
+  char zL, zC;
+
+  if(n <= 0)
+    return 1;
+
+  zL = !L || !m;
+  zC = !C || !v;
+
+  if(!zL) zL = zL || ! NumberOfRows(*L) || ! NumberOfColumns(*L);
+  if(!zC) zC = zC || ! NumberOfRows(*C) || ! NumberOfColumns(*C);
+
+  if(!B || (zL && zC)) 
+    return zL && zC && !B;
+
+  if(!zL)
+    n = NumberOfRows(*L);
+  else
+    n = NumberOfRows(*C);
+
+  for(i = 0; i < n; i++) {
+    a = 0;
+    if(!zL)
+      a = MultiplyVector(L, (matrix*) m, i, -1, 0);
+    if(!zC)
+      a += MultiplyVector(C, (matrix*) v, i, -1, 0);
+    if(!TestCondition(a, type, B[i]))
+      return 0;
+  }
+  return 1;
+}
+
+
+/***************************************************************************
  GETSUPERVISOR
 ****************************************************************************/
 
@@ -1370,7 +1467,13 @@
    closed-loop input (Dcp) and output (Dcm) matrices and from the initial 
    marking of the closed-loop (ms0). 
 
-   This function assumes free-labeled PNs. */
+   This function assumes that the set of transitions of the closed-loop is 
+   the same as the set of transitions of the plant. Two cases in which
+   this is true are the following: 
+   - free-labeled closed-loop PN. 
+   - the supervisor implements Lm + Hq + Cv \leq b via SBPI. (Since SBPI does 
+   not add new transitions). 
+*/
 
   pns *apnsv;
   int tnum, i, j, k, l, t, pcn, tcn, flag, *labels;
@@ -1750,7 +1853,12 @@
 }
 
 
+//=========================================================================
 
+
+int TestConstraint();
+
+
 /* Things to do:
    - composepn ignores the text fields of the pns. 
    - composepn assumes that the places in the two pns are distinct.

Modified: pnheaders/pns.h
===================================================================
--- pnheaders/pns.h	2011-04-08 22:36:44 UTC (rev 246)
+++ pnheaders/pns.h	2011-05-11 12:20:38 UTC (rev 247)
@@ -359,6 +359,7 @@
   int type:1; /* type = 1 indicates an external process */
   int start:1; /* start = 1 if the supervisor should start this process */
   char thread:1; /* set to 1 if process should be implemented as a thread */
+  char supervisor:1; /* set to 1 if the process is a supervisor component */
 } process;
 
 
@@ -388,14 +389,37 @@
    use n < 0. The pn parameter specifies the PN on which the constraints
    are defined. If one or more of L, H, or C is unavailable, enter 0. */
 
+int TestLCB(matrix* L, int* m, matrix* C, int* v, int type, int* B);
 
+/* 'type' should be GREATER, LESS, EQUAL, GREATER_OR_EQUAL, or LESS_OR_EQUAL
+   (which are defined in matrix.h).
+
+   The function calculates L*m + C*v and compares the result to B.
+   If all elements of the result satisfy the 'type' constraint when compared
+   to B, then the function returns 1. Otherwise, it returns zero. 
+
+   Unused entries may be set to zero. For instance, TestLCB(L,m,0,0,LESS,B,n)
+   checks whether L*m < B. */ 
+
+
+pns pn_composition(process** process_array, int num);
+/* Composes the PNs in the process array and returns the result. */
+
+
 pns* getSupervisor(pns* pn, matrix* Dcm, matrix* Dcp, int* ms0);
 
 /* Extracts the PN representing the supervisor from the plant PN (pn), the 
    closed-loop input (Dcp) and output (Dcm) matrices and from the initial 
-   marking of the closed-loop (ms0). This function assumes free-labeled PNs. */
+   marking of the closed-loop (ms0). 
 
+   This function assumes that the set of transitions of the closed-loop is 
+   the same as the set of transitions of the plant. Two cases in which
+   this is true are the following: 
+   - free-labeled closed-loop PN. 
+   - the supervisor implements Lm + Hq + Cv \leq b via SBPI. (Since SBPI does 
+   not add new transitions).  */
 
+
 void dealloc_specs(specs* sp);
 
 void dealloc_process(process* p);

Modified: spnbox/linenf.c
===================================================================
--- spnbox/linenf.c	2011-04-08 22:36:44 UTC (rev 246)
+++ spnbox/linenf.c	2011-05-11 12:20:38 UTC (rev 247)
@@ -670,7 +670,7 @@
 		}
 	}
 	/*If m0 is given, b must be given*/
-	if(m0 && ! b)
+	if(m0 && ! b && Constraints)
 	{
 		merror(0, "LINENF: The constraint vector b must be given if an initial marking m0 is given");
 		return -1;

Modified: spnbox/spnbox.h
===================================================================
--- spnbox/spnbox.h	2011-04-08 22:36:44 UTC (rev 246)
+++ spnbox/spnbox.h	2011-05-11 12:20:38 UTC (rev 247)
@@ -702,7 +702,7 @@
 array.
 
 
-Written for Matlab by Marian V. Iordache, mio...@nd...
+Written for Matlab by Marian V. Iordache
 Original Matlab code extended the Matlab pn2acpn code written on
 M. Iordache -- Sep. 4, 2000
 and revised on Oct. 24, 2001
@@ -1192,7 +1192,7 @@
 /*
 GCDV  greatest common divisor of a vector/matrix. Uses GCD.
 
-Written by Marian V. Iordache, mio...@nd...
+Written by Marian V. Iordache
 
 C Usage:
 If m is a null pointer, the function returns the gcd of the row and column


This was sent by the SourceForge.net collaborative development platform, the world's largest Open Source development site.