[Pntool-developers] SF.net SVN: pntool:[261] present_version/spnbox
Brought to you by:
compaqdrew,
miordache
Menu
▾
▴
[Pntool-developers] SF.net SVN: pntool:[261] present_version/spnbox
|
From: <mio...@us...> - 2011-08-04 23:18:42
|
Revision: 261
http://pntool.svn.sourceforge.net/pntool/?rev=261&view=rev
Author: miordache
Date: 2011-08-04 23:18:35 +0000 (Thu, 04 Aug 2011)
Log Message:
-----------
Modified Paths:
--------------
old_versions/2011/spnbox/spnbox.h
present_version/spnbox/spnbox.h
Removed Paths:
-------------
present_version/pnheaders/main_function.c
Modified: old_versions/2011/spnbox/spnbox.h
===================================================================
--- old_versions/2011/spnbox/spnbox.h 2011-07-28 21:14:17 UTC (rev 260)
+++ old_versions/2011/spnbox/spnbox.h 2011-08-04 23:18:35 UTC (rev 261)
@@ -1,14 +1,23 @@
#ifndef SPNBOX_H
#define SPNBOX_H
+// Written by Steven Camp in 2009.
+
+/* 2011 Change: The following change was made in order to ensure UpdateDPData
+ of dp.c is portable (to avoid "segmentation faults" on certain systems)
+ "__attribute__ ((packed))" was inserted in the fields of the data structures
+ used by UpdateDPData. Note that UpdateDPData assumes that the bytes of one
+ field precede immediately the bytes of the next field. The change ensures
+ that this assumption is correct. M.V. Iordache, August 2011. */
+
#include <stdarg.h>
#include "../pnheaders/matrix.h"
-#include "../../../present_version/third-party/lp_solve_5.5/lpkit.h"
+#include "../third-party/lp_solve_5.5/lpkit.h"
#include "../pnheaders/pns.h"
typedef struct supervis_r { /* result of supervis */
- matrix Dfm; //The supervised net output matrix
- matrix Dfp; //The supervised net input matrix
+ matrix Dfm __attribute__ ((packed)); //The supervised net output matrix
+ matrix Dfp __attribute__ ((packed)); //The supervised net input matrix
} supervis_r;
typedef struct ipslv_r {
@@ -51,24 +60,24 @@
typedef struct msplit_r
{
/*Final Petri net*/
- matrix Df;
- matrix Dfm;
- matrix Dfp;
+ matrix Df __attribute__ ((packed));
+ matrix Dfm __attribute__ ((packed));
+ matrix Dfp __attribute__ ((packed));
/*The transformation matrix for finding the dependent marking
from the independent marking*/
- matrix Mf;
+ matrix Mf __attribute__ ((packed));
/*Initial and universal marking constraints*/
- matrix L0f;
- matrix Lf;
+ matrix L0f __attribute__ ((packed));
+ matrix Lf __attribute__ ((packed));
/*The modified list of independent places and the count.*/
- int* iplf;
- int ipCountf;
+ int* iplf __attribute__ ((packed));
+ int ipCountf __attribute__ ((packed));
/*The lists of transitions that cannot be made live if a
specified transition is dead, indexed by the specified transition.
The number of lists is the number of transitions*/
- int **TDf;
+ int **TDf __attribute__ ((packed));
/*This gives the number of elements in each list above*/
- int* TDfCount;
+ int* TDfCount __attribute__ ((packed));
} msplit_r;
typedef struct nltrans_r
@@ -80,42 +89,42 @@
typedef struct pn2acpn_r
{
//The final Petri net matrices
- matrix Df;
- matrix Dmf;
- matrix Dpf;
+ matrix Df __attribute__ ((packed));
+ matrix Dmf __attribute__ ((packed));
+ matrix Dpf __attribute__ ((packed));
//Modified constraint matrices
- matrix MXF;
- matrix L0F;
- matrix LF;
+ matrix MXF __attribute__ ((packed));
+ matrix L0F __attribute__ ((packed));
+ matrix LF __attribute__ ((packed));
//The new independent place list, given as a pointer to an array of integers
- int *iplf;
+ int *iplf __attribute__ ((packed));
//The number of independent places (length of the iplf array)
- int iplfCount;
+ int iplfCount __attribute__ ((packed));
} pn2acpn_r;
typedef struct pn2eacpn_r
{
//New Petri net matrices
- matrix Df;
- matrix Dmf;
- matrix Dpf;
+ matrix Df __attribute__ ((packed));
+ matrix Dmf __attribute__ ((packed));
+ matrix Dpf __attribute__ ((packed));
//New constraint matrices
- matrix MXF;
- matrix L0F;
- matrix LF;
+ matrix MXF __attribute__ ((packed));
+ matrix L0F __attribute__ ((packed));
+ matrix LF __attribute__ ((packed));
//New independent place list, given as a pointer to an array of integers.
- int *iplf;
+ int *iplf __attribute__ ((packed));
//Length of the independent place list.
- int iplfCount;
+ int iplfCount __attribute__ ((packed));
/*New list of transitions that are unraisable when a given transition is dead.
This is a pointer to an array of integer arrays. There is an element for each
transition. Each array lists the transitions that cannot be raised if the
transition that array corresponds to is dead.*/
- int **TD;
+ int **TD __attribute__ ((packed));
/*The number of elements in each of the arrays in the TD array of arrays.
This is a pointer to an array of integers, one for each transition, that lists
the number of elements in the corresponding array in TD.*/
- int *TDCount;
+ int *TDCount __attribute__ ((packed));
} pn2eacpn_r;
typedef struct chkcons_r
@@ -144,20 +153,20 @@
{
/*The input and output matrices of the active subnet, given as a copy of the
original subnet with dead transitions and/or places overwritten with zeroes.*/
- matrix Dma;
- matrix Dpa;
+ matrix Dma __attribute__ ((packed));
+ matrix Dpa __attribute__ ((packed));
/*The input and output matrices of the active subnet, given as those rows from
Dma and Dpa that were not overwritten with zeroes.*/
- matrix Dmra;
- matrix Dpra;
+ matrix Dmra __attribute__ ((packed));
+ matrix Dpra __attribute__ ((packed));
/*The list of active transitions. This is a pointer to an array of integers,
each one of which is the index of a transition that made it into the active
subnet.*/
- int* TA;
+ int* TA __attribute__ ((packed));
/*The number of active transitions, i.e. length of the TA list.*/
- int TACount;
+ int TACount __attribute__ ((packed));
/*This flag will be meaninful only if a uniqueness check was done. See actn.*/
- int unique;
+ int unique __attribute__ ((packed));
} actn_r;
/*The type of data returned by actn and tactn are identical. Create a tactn_r
@@ -179,18 +188,18 @@
those that were added by the asiph procedure. Given as a matrix with a row
for each place and a column for each siphon. An element will be nonzero if
the corresponding place is a part of the corresponding siphon.*/
- matrix MS;
+ matrix MS __attribute__ ((packed));
/*The list of active siphons added by the asiph procedure. Same format as MS.*/
- matrix NMS;
+ matrix NMS __attribute__ ((packed));
} asiph_r;
typedef struct admcon_r
{
/*A flag vector and its length.*/
- int *l;
- int lCount;
+ int *l __attribute__ ((packed));
+ int lCount __attribute__ ((packed));
/*A flag. If set, we found an admissible constraint.*/
- int how;
+ int how __attribute__ ((packed));
} admcon_r;
typedef struct dp_r
@@ -477,6 +486,13 @@
Written by Feng Zhu, fz...@nd...
Converted to C by Po Wu, pw...@nd... */
+
+int satisfied_expr(expression2 *expr);
+/* Returns 1 if the expression is satisfied at the initial marking. Otherwise,
+ it returns 0. Written by Po Wu. Placed in tree2spec.c. The test file is
+ test-lintree.c. */
+
+
linenf_r linenf(matrix* Dm, matrix* Dp, matrix* L, int* b, int* m0, matrix* F, matrix* C, int TucCount, int* Tuc, int TuoCount, int* Tuo);
/* LINENF - Linear Inequality Enforcement
This function creates the supervisor enforcing
Deleted: present_version/pnheaders/main_function.c
===================================================================
--- present_version/pnheaders/main_function.c 2011-07-28 21:14:17 UTC (rev 260)
+++ present_version/pnheaders/main_function.c 2011-08-04 23:18:35 UTC (rev 261)
@@ -1,567 +0,0 @@
-#include "pns.h"
-#include "spnbox.h"
-#include "codegen.h"
-#include"insert.h"
-
-int verb;
-
-int inline is_verbose() { return verb; }
-
-
-
-
-void br_filter(char *p) { // removes beginning and end braces
- int n;
- if(!p)
- return;
- n = strlen(p);
- if(!n)
- return;
- n--;
- if(p[0] == '{' && p[n] == '}') {
- p[0] = ' ';
- p[n] = ' ';
- }
-}
-
-
-int is_empty(char *p) { // returns 1 if p has only space and tab characters
- int i;
- if(!p) return 1;
- for(i = 0; p[i]; i++)
- if(p[i] != ' ' && p[i] != '\t')
- break;
- return ! p[i];
-}
-
-int th_filter(char** ap, char* pattern) { // remove pattern from strings
- char* p = *ap, *p2 = 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, 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;
- }
- break;
- }
- return 0;
-}
-
-
-void main_filter(char **inc, char **newinc, char **main, char *pattern) {
- // Copy/append to newinc everything in *inc up to 'pattern'.
- // Copy/append to *main everything in *inc following 'pattern'.
- // If newinc is zero, keep in inc everything up to 'pattern'.
- // If newinc is nonzero, dealloc *inc and set it to zero.
-
- int i, n;
- char *p, *p2;
-
- if(!inc) return;
- p = *inc;
- if(!p || !pattern) return;
- n = strlen(pattern);
- for(i = 0; p[i]; i++) {
- if(p[i] == ' ' || p[i] == '\t')
- continue;
- if(!strncmp(p+i, pattern, n)) // then 'pattern' has been found
- break;
- }
-
- if(main && p[i]) { // p[i] is nonzero if 'pattern' was found
- if(*main) { // append to text in *main
- asprintf(&p2, "%s\n\n%s", *main, p+i+n);
- free(*main);
- *main = p2;
- }
- else // write text to *main
- asprintf(main, "%s", p+i+n);
- }
-
- p[i] = 0; // keep in inc everything up to 'pattern'
- if(newinc) {
- if(!*newinc)
- *newinc = *inc;
- else { // append to text in newinc
- asprintf(&p2, "%s\n\n%s", *newinc, *inc);
- free(*newinc);
- *newinc = p2;
- free(*inc);
- }
- *inc = 0;
- }
-}
-
-
-void sp_filter(specs *sp) {
- // Removes beginning and end braces. Processes embedded instructions.
- // Sets default values for fields not processed by the translator.
- int i, j;
- pns *pn;
- arcs *pa;
- if(!sp)
- return;
- if(!sp->process_array)
- return;
-
- // Default values
-
- sp->main = 0;
- sp->include = 0;
-
- for(i = 0; i < sp->process_num; i++) {
- if(!sp->process_array[i])
- continue;
-
- sp->process_array[i]->main = 0; // not processed by the translator
-
- br_filter(sp->process_array[i]->build);
- br_filter(sp->process_array[i]->include);
-
- // 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>");
- // Process the <main> instructions if any
- if(sp->process_array[i]->supervisor)
- main_filter(&(sp->process_array[i]->include), &(sp->include), \
- &(sp->main), "<main>");
- else
- main_filter(&(sp->process_array[i]->include), 0, \
- &(sp->process_array[i]->main), "<main>");
- pn = sp->process_array[i]->pn;
- if(pn) {
- if(pn->segment)
- for(j = 0; j < pn->pnum; j++)
- br_filter(pn->segment[j]);
- if(pn->select)
- for(j = 0; j < pn->pnum; j++)
- br_filter(pn->select[j]);
- if(pn->arc_list)
- for(j = 0; j < pn->tnum; j++)
- for(pa = pn->arc_list[j]; pa; pa = pa->next)
- br_filter(pa->condition);
- }
- }
-}
-
-
-int main(int na, char* argv[]) {
-
- 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, pn1, *apnsv;
- process **plant_array, **spv_array;
- matrix L, C, H;
- int *B;
- struct myinsert ins;
- 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;
-
- // These are flags
- unsigned char no_main = 0, signals = 0, sleep = 1, single_ch = 0;
-
-char help[] = "\
-The program generates concurrency control code based on a specification file.\
-\n\
-\nUsage: ct [options] [specification file] [-b list]\
-\n\
-\n'list' stands for a list of files and compiler options that should be\
-\ncopied to the command line used to build the executable file.\
-\n\
-\nOptions:\
-\n -d<number> Comment on execution progress. More information displayed for\
-\n higher values of <number>, where <number> = 1 ... 20.\
-\n -m Do not generate a main function.\
-\n -s<number> Depending on the value of <number> the supervisor can be built\
-\n as follows:\
-\n 0: The supervisor waits actively for events. \
-\n 1: The supervisor is built as in option 0 except it enters a \
-\n sleep state (for a finite amount of time) when no events\
-\n are detected. \
-\n 2: The supervisor blocks when no events occur. This option is \
-\n best when the number of concurrent processes or threads is \
-\n small. The supervisor has the least computational overhead \
-\n under this option. \
-\n\
-\nExamples: ct manf.sp\
-\n ct -d3 input.sp\n";
-
-// About single channe (option 2) all plant components write to the same pipe.
-// Use this option if it is unlikely that the pipe would keep getting full
-// (i.e. if there are not many processes). Otherwise, fairness depends on
-// whether the OS is fair in deciding which requests to serve when the pipe
-// keeps getting full and there are competing requests to write to the pipe.
-
-
- // 1. INITIALIZATION
-
- ins = InitInsert(512); // used to store command line parameters
- verb = 0;
- input = 0;
-
- if(na <= 1) {
- puts(help);
- finish = 1;
- }
-
- for(i = 1; i < na && !finish; i++) {
- if(!strcmp(argv[i], "--help")) {
- finish = 1;
- puts(help);
- break;
- }
- if(argv[i][0] == '-') {
- switch(argv[i][1]) {
- case 'd': verb = atoi(argv[i]+2);
- break;
- case 'm': no_main = 1;
- break;
- case 's': j = atoi(argv[i]+2);
- switch(j) {
- case 0: sleep = 0; break;
- case 1: sleep = 1; break;
- case 2: single_ch = 1; break;
- case 3: signals = 1; break;
- default: fprintf(stderr,"Unexpected parameter %s.\n", argv[i]);
- }
- break;
- case 'b': if(argv[i][2])
- ins = FSInsert(ins, " %s", argv[i]+2);
- for(i = i + 1; i < na; i++)
- ins = FSInsert(ins, " %s", argv[i]);
- break;
- default: fprintf(stderr, "Unknown option %s.\n", argv[i]);
- }
- }
- else {
- if(input)
- fprintf(stderr, "Unexpected parameter %s.\n", argv[i]);
- else
- input = argv[i];
- }
- }
-
- if(!input) {
- fprintf(stderr, "No input file specified.");
- finish = 1;
- }
- else {
- f = fopen(input,"r");
- if(!f) {
- fprintf(stderr, "The file %s cannot be opened.\n", input);
- finish = 1;
- }
- else {
- if(verb && !finish)
- fprintf(stderr, "Using the input file %s ...\n", input);
- fclose(f);
- }
- }
-
- build = GetInsertBuf(&ins);
-
- if(finish) { // Terminate if errors were encountered
- if(build) free(build);
- return 0;
- }
-
- // 2. TRANSLATE SPECIFICATION
-
- sp = ScanInput(input);
-
- // 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);
- if(build) free(build);
- return 0;
- }
-
- // Set settings not detected by translator
-
- sp->signals = signals;
- sp->sleep = sleep;
- sp->singlechannel = single_ch;
- sp->nomain = no_main;
-
- 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======================================================");
- 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;
-
- 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);
-
- // 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) {
- l1 = snc->pn1->t[snc->t1].l; l2 = snc->pn2->t[snc->t2].l;
- if(l1 != l2) {
- i = 1;
- j = (l1 > l2)?l1:l2;
- snc->pn1->t[snc->t1].l = j; snc->pn2->t[snc->t2].l = j;
- }
- }
-
- // 2.3 Obtain SC specification. Currently:
- // extract the L, C, H, and b matrices (more complex specs to be done later)
- // the function calculates also the composed PN
-
- extractLHCB(sp, &pn, &L, &H, &C, &B);
-
- if(is_verbose() >= 3) { // For debugging
- printf("\n\n======================================================");
- printf("\nCONSTRAINTS:\n");
- printLHCB(&pn, &L, &H, &C, B, -1, stdout);
- }
-
- // 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);
-
- if(is_verbose() >= 3) { // For debugging
- printf("\n\n======================================================");
- printf("\nADMISSIBLE CONSTRAINTS (H entries omitted): \n");
- printLHCB(&pn, &lin_res.Lf, 0, &lin_res.Cf, lin_res.bf, -1, stdout);
- }
-
- // 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");
-
- // 3.2. Enforce liveness
-
- // - 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
-
- // 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 PLANT PN PLUS PREDEFINED SUPERVISOR COMPONENTS\n");
- displaypn(pn, stdout);
- printf("\n\n======================================================");
- if(apnsv) {
- printf("\nSC GENERATED SUPERVISOR\n");
- displaypn(*apnsv, stdout);
- }
- else
- printf("\nNO SC GENERATED SUPERVISOR\n");
- }
- deallocpn(&pn);
-
-
- // 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++;
- }
- }
-
- // 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);
- */
-
- lls = get_label_list(plant_array, plcnum);
- syncl = get_synclist(lls, plant_array);
- TInf = get_TrData(apnsv, plant_array, plcnum, lls);
-
- // Call the code generation function
-
- /*CodeGenerator(apnsv, sp->name, sp->process_array, sp->process_num, \
- syncl, TInf, build);
- */
- sp->sbuildparam = build;
- CodeGenerator(apnsv, sp, plant_array, plcnum, syncl, TInf);
-
-
- // 5. TERMINATE
-
- if(apnsv) {
- deallocpn(apnsv);
- //free(apnsv);
- }
- free(plant_array);
- free(spv_array);
- dealloc_specs(sp);
- free_label_list(lls);
- free_synclist(syncl);
- 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: present_version/spnbox/spnbox.h
===================================================================
--- present_version/spnbox/spnbox.h 2011-07-28 21:14:17 UTC (rev 260)
+++ present_version/spnbox/spnbox.h 2011-08-04 23:18:35 UTC (rev 261)
@@ -1,14 +1,23 @@
#ifndef SPNBOX_H
#define SPNBOX_H
+// Written by Steven Camp in 2009.
+
+/* 2011 Change: The following change was made in order to ensure UpdateDPData
+ of dp.c is portable (to avoid "segmentation faults" on certain systems)
+ "__attribute__ ((packed))" was inserted in the fields of the data structures
+ used by UpdateDPData. Note that UpdateDPData assumes that the bytes of one
+ field precede immediately the bytes of the next field. The change ensures
+ that this assumption is correct. M.V. Iordache, August 2011. */
+
#include <stdarg.h>
#include "../pnheaders/matrix.h"
#include "../third-party/lp_solve_5.5/lpkit.h"
#include "../pnheaders/pns.h"
typedef struct supervis_r { /* result of supervis */
- matrix Dfm; //The supervised net output matrix
- matrix Dfp; //The supervised net input matrix
+ matrix Dfm __attribute__ ((packed)); //The supervised net output matrix
+ matrix Dfp __attribute__ ((packed)); //The supervised net input matrix
} supervis_r;
typedef struct ipslv_r {
@@ -51,24 +60,24 @@
typedef struct msplit_r
{
/*Final Petri net*/
- matrix Df;
- matrix Dfm;
- matrix Dfp;
+ matrix Df __attribute__ ((packed));
+ matrix Dfm __attribute__ ((packed));
+ matrix Dfp __attribute__ ((packed));
/*The transformation matrix for finding the dependent marking
from the independent marking*/
- matrix Mf;
+ matrix Mf __attribute__ ((packed));
/*Initial and universal marking constraints*/
- matrix L0f;
- matrix Lf;
+ matrix L0f __attribute__ ((packed));
+ matrix Lf __attribute__ ((packed));
/*The modified list of independent places and the count.*/
- int* iplf;
- int ipCountf;
+ int* iplf __attribute__ ((packed));
+ int ipCountf __attribute__ ((packed));
/*The lists of transitions that cannot be made live if a
specified transition is dead, indexed by the specified transition.
The number of lists is the number of transitions*/
- int **TDf;
+ int **TDf __attribute__ ((packed));
/*This gives the number of elements in each list above*/
- int* TDfCount;
+ int* TDfCount __attribute__ ((packed));
} msplit_r;
typedef struct nltrans_r
@@ -80,42 +89,42 @@
typedef struct pn2acpn_r
{
//The final Petri net matrices
- matrix Df;
- matrix Dmf;
- matrix Dpf;
+ matrix Df __attribute__ ((packed));
+ matrix Dmf __attribute__ ((packed));
+ matrix Dpf __attribute__ ((packed));
//Modified constraint matrices
- matrix MXF;
- matrix L0F;
- matrix LF;
+ matrix MXF __attribute__ ((packed));
+ matrix L0F __attribute__ ((packed));
+ matrix LF __attribute__ ((packed));
//The new independent place list, given as a pointer to an array of integers
- int *iplf;
+ int *iplf __attribute__ ((packed));
//The number of independent places (length of the iplf array)
- int iplfCount;
+ int iplfCount __attribute__ ((packed));
} pn2acpn_r;
typedef struct pn2eacpn_r
{
//New Petri net matrices
- matrix Df;
- matrix Dmf;
- matrix Dpf;
+ matrix Df __attribute__ ((packed));
+ matrix Dmf __attribute__ ((packed));
+ matrix Dpf __attribute__ ((packed));
//New constraint matrices
- matrix MXF;
- matrix L0F;
- matrix LF;
+ matrix MXF __attribute__ ((packed));
+ matrix L0F __attribute__ ((packed));
+ matrix LF __attribute__ ((packed));
//New independent place list, given as a pointer to an array of integers.
- int *iplf;
+ int *iplf __attribute__ ((packed));
//Length of the independent place list.
- int iplfCount;
+ int iplfCount __attribute__ ((packed));
/*New list of transitions that are unraisable when a given transition is dead.
This is a pointer to an array of integer arrays. There is an element for each
transition. Each array lists the transitions that cannot be raised if the
transition that array corresponds to is dead.*/
- int **TD;
+ int **TD __attribute__ ((packed));
/*The number of elements in each of the arrays in the TD array of arrays.
This is a pointer to an array of integers, one for each transition, that lists
the number of elements in the corresponding array in TD.*/
- int *TDCount;
+ int *TDCount __attribute__ ((packed));
} pn2eacpn_r;
typedef struct chkcons_r
@@ -144,20 +153,20 @@
{
/*The input and output matrices of the active subnet, given as a copy of the
original subnet with dead transitions and/or places overwritten with zeroes.*/
- matrix Dma;
- matrix Dpa;
+ matrix Dma __attribute__ ((packed));
+ matrix Dpa __attribute__ ((packed));
/*The input and output matrices of the active subnet, given as those rows from
Dma and Dpa that were not overwritten with zeroes.*/
- matrix Dmra;
- matrix Dpra;
+ matrix Dmra __attribute__ ((packed));
+ matrix Dpra __attribute__ ((packed));
/*The list of active transitions. This is a pointer to an array of integers,
each one of which is the index of a transition that made it into the active
subnet.*/
- int* TA;
+ int* TA __attribute__ ((packed));
/*The number of active transitions, i.e. length of the TA list.*/
- int TACount;
+ int TACount __attribute__ ((packed));
/*This flag will be meaninful only if a uniqueness check was done. See actn.*/
- int unique;
+ int unique __attribute__ ((packed));
} actn_r;
/*The type of data returned by actn and tactn are identical. Create a tactn_r
@@ -179,18 +188,18 @@
those that were added by the asiph procedure. Given as a matrix with a row
for each place and a column for each siphon. An element will be nonzero if
the corresponding place is a part of the corresponding siphon.*/
- matrix MS;
+ matrix MS __attribute__ ((packed));
/*The list of active siphons added by the asiph procedure. Same format as MS.*/
- matrix NMS;
+ matrix NMS __attribute__ ((packed));
} asiph_r;
typedef struct admcon_r
{
/*A flag vector and its length.*/
- int *l;
- int lCount;
+ int *l __attribute__ ((packed));
+ int lCount __attribute__ ((packed));
/*A flag. If set, we found an admissible constraint.*/
- int how;
+ int how __attribute__ ((packed));
} admcon_r;
typedef struct dp_r
This was sent by the SourceForge.net collaborative development platform, the world's largest Open Source development site.
|