Skip to content

HTTPS clone URL

Subversion checkout URL

You can clone with HTTPS or Subversion.

Download ZIP
Browse files

First commit

  • Loading branch information...
commit 8fbcef9830ab451a517344e10773677f4f2ce68f 0 parents
madewulf@madewulf-desktop authored
Showing with 7,957 additions and 0 deletions.
  1. +116 −0 automata/automata.c
  2. +75 −0 automata/automata.h
  3. +225 −0 avl/avl.c
  4. +33 −0 avl/avl.h
  5. +5 −0 avl/fatal.h
  6. +421 −0 constraints/constraints.c
  7. +35 −0 constraints/constraints.h
  8. 0  constraints/inequalities.h
  9. +9 −0 constraints/term.h
  10. 0  constraints/terms.h
  11. +17 −0 enums.h
  12. +118 −0 examples/audio.el
  13. +66 −0 examples/exemple1.el
  14. +73 −0 examples/exemple2.el
  15. +277 −0 examples/proto2.el
  16. +189 −0 main.c
  17. +86 −0 makefile
  18. +16 −0 parser/parser.h
  19. +1,413 −0 parser/parser.y
  20. +23 −0 preProcessing/preProcessing.h
  21. +91 −0 preProcessing/preProcessing.lex
  22. +188 −0 preProcessing/preProcessing.y
  23. +93 −0 preProcessing/tableOfConstants.c
  24. +23 −0 preProcessing/tableOfConstants.h
  25. +208 −0 rationals/rationals.c
  26. +48 −0 rationals/rationals.h
  27. +443 −0 scanner/scanner.lex
  28. +20 −0 system/system.c
  29. +18 −0 system/system.h
  30. +97 −0 toUppaal/rationalTreatment.c
  31. +6 −0 toUppaal/rationalTreatment.h
  32. +769 −0 toUppaal/toUppaal.c
  33. +10 −0 toUppaal/toUppaal.h
  34. +1,354 −0 toWatchers/toWatchers.c
  35. +7 −0 toWatchers/toWatchers.h
  36. +87 −0 utils/labStatus.c
  37. +21 −0 utils/labStatus.h
  38. +211 −0 utils/utils.c
  39. +47 −0 utils/utils.h
  40. +410 −0 writeHyTech/writeHyTech.c
  41. +16 −0 writeHyTech/writeHyTech.h
  42. +580 −0 writeUppaal/writeUppaal.c
  43. +13 −0 writeUppaal/writeUppaal.h
116 automata/automata.c
@@ -0,0 +1,116 @@
+#include "automata.h"
+
+
+struct var * makeVar(int id, struct var * next)
+{
+ struct var * res;
+ res= (struct var * ) malloc (sizeof(struct var));
+ if (!res)
+ {
+ fprintf(stderr,"Not enough memory! \n");
+ exit(-1);
+ }
+ res->id=id;
+ res->next=next;
+ return res;
+}
+
+struct lab * makeLabel(int id, enum labelType type, struct lab * next)
+{
+ struct lab * res;
+ res= (struct lab * ) malloc (sizeof(struct lab));
+ if (!res)
+ {
+ fprintf(stderr,"Not enough memory! \n");
+ exit(-1);
+ }
+ res->id=id;
+ res->next=next;
+ res->type=type;
+ return res;
+}
+
+struct transition * makeTransition(int idDest,
+ int idLabel,
+ enum transitionStatus ts,
+ expr guard,
+ expr update,
+ struct transition* next)
+{
+ struct transition * res;
+ res= (struct transition * ) malloc (sizeof(struct transition));
+ if (!res)
+ {
+ fprintf(stderr,"Not enough memory! \n");
+ exit(-1);
+ }
+ res->idDest=idDest;
+ res->idLabel=idLabel;
+ res->ts=ts;
+ res->guard=guard;
+ res->update=update;
+ res->next=next;
+ return res;
+}
+
+struct location * makeLocation( int id,
+ expr inv,
+ expr rateCond,
+ struct transition * transitions,
+ struct location * next)
+{
+ struct location * res;
+ res= (struct location * ) malloc (sizeof(struct location));
+ if (!res)
+ {
+ fprintf(stderr,"Not enough memory! \n");
+ exit(-1);
+ }
+ res->id=id;
+ res->inv=inv;
+ res->rateCond=rateCond;
+ res->transitions=transitions;
+ res->type=SLW;
+ res->next=next;
+ return res;
+}
+
+struct automaton * makeAutomaton( int id,
+ enum automType type,
+ expr initialisation,
+ int idInitLoc,
+ struct lab * labList,
+ struct location * locations,
+ struct automaton * next)
+{
+ struct automaton * res;
+ res= (struct automaton * ) malloc (sizeof(struct automaton));
+ if (!res)
+ {
+ fprintf(stderr,"Not enough memory! \n");
+ exit(-1);
+ }
+ res->id=id;
+ res->type=type;
+ res->initialisation=initialisation;
+ res->idInitLoc=idInitLoc;
+ res->labList=labList;
+ res->locations=locations;
+ res->next=next;
+ return res;
+}
+
+struct lab * appendLabList(struct lab * l1, struct lab * l2)
+{
+ struct lab * res;
+ if (!l1)
+ res=l2;
+ else
+ {
+ res=l1;
+ while(l1->next)
+ l1=l1->next;
+ l1->next=l2;
+ }
+ return res;
+}
75 automata/automata.h
@@ -0,0 +1,75 @@
+#ifndef __AUTOMATA_H
+#define __AUTOMATA_H
+
+#include "../constraints/constraints.h"
+
+struct var
+{
+ int id;
+ struct var * next; /*pour constituer des listes de variable*/
+};
+
+struct lab
+{
+ int id;
+ enum labelType type;
+ struct lab * next;
+};
+
+struct transition
+{
+ int idDest; /*l'identifiant de la destination*/
+ int idLabel; /*l'identifiant du label*/
+ enum transitionStatus ts; /*ORDINARY, ASAP,BROADCASTEMITTER,BROADCASTRECEIVER*/
+ expr guard;
+ expr update;
+ struct transition * next; /*pour constituer des listes de transitions*/
+};
+
+struct location
+{
+ int id;/*l'identifiant de la location*/
+ expr inv;
+ expr rateCond;
+ struct transition * transitions;
+ enum locationType type;/*SLW ou URG*/
+ struct location * next; /*pour constituer des listes de location*/
+};
+
+struct automaton
+{
+ int id;
+ enum automType type;
+ expr initialisation;
+ int idInitLoc;
+ int idParameter;
+ struct lab * labList; /*la liste des labels*/
+ struct location * locations;
+ struct automaton * next; /*pour constituer des listes d'automates*/
+};
+
+struct var * makeVar(int id,
+ struct var * next);
+struct lab * makeLabel(int id, enum labelType type, struct lab * next);
+struct transition * makeTransition(int idDest,
+ int idLabel,
+ enum transitionStatus ts,
+ expr guard,
+ expr udpate,
+ struct transition* next);
+struct location * makeLocation( int id,
+ expr inv,
+ expr rateCond,
+ struct transition * transitions,
+ struct location * next);
+struct automaton * makeAutomaton(int id,
+ enum automType type,
+ expr initialisation,
+ int idInitLoc,
+ struct lab * labList,
+ struct location * locations,
+ struct automaton * next);
+
+struct lab * appendLabList(struct lab * l1, struct lab * l2);
+
+#endif
225 avl/avl.c
@@ -0,0 +1,225 @@
+#include "avl.h"
+#include <stdlib.h>
+#include "fatal.h"
+#include "../enums.h"
+
+int prof=0;
+int count=0;
+
+AvlTree makeAvlNode(int id, string s, enum nameType ty)
+{
+ AvlTree res;
+ res= (AvlTree) malloc(sizeof(struct AvlNode));
+ if (!res)
+ {
+ fprintf(stderr, "Not enough memory!\n");
+ exit(-1);
+ }
+ switch(ty)
+ {
+ case LOCATION :
+ {
+ res->data.locPtr=(struct location *) malloc(sizeof(struct location));
+ if (!res->data.locPtr)
+ {
+ fprintf(stderr, "Not enough memory!\n");
+ exit(-1);
+ }
+ break ;
+ }
+ case AUTOMATON :
+ {
+ res->data.automPtr=(struct automaton *) malloc (sizeof(struct automaton));
+ if (!res->data.automPtr)
+ {
+ fprintf(stderr, "Not enough memory!\n");
+ exit(-1);
+ }
+ break;
+ }
+ default :
+ break;
+ }
+ res->Left=NULL;
+ res->Right=NULL;
+ res->Height=0;
+ res->id=id;
+ res->type=ty;
+ res->name=(string) malloc (sizeof(char)* (strlen(s)+1));
+ strcpy(res->name,s);
+ return res;
+}
+
+AvlTree
+Find (int X, AvlTree T)
+{
+ if (T == NULL)
+ return NULL;
+ if (X < T->id)
+ return Find (X, T->Left);
+ else if (X > T->id)
+ return Find (X, T->Right);
+ else
+ return T;
+}
+
+static int
+Height (AvlTree P)
+{
+ if (P == NULL)
+ return -1;
+ else
+ return P->Height;
+}
+
+static int
+Max (int Lhs, int Rhs)
+{
+ return Lhs > Rhs ? Lhs : Rhs;
+}
+
+
+/* This function can be called only if K2 has a left child */
+/* Perform a rotate between a node (K2) and its left child */
+/* Update heights, then return new root */
+
+static AvlTree
+SingleRotateWithLeft (AvlTree K2)
+{
+ AvlTree K1;
+
+ K1 = K2->Left;
+ K2->Left = K1->Right;
+ K1->Right = K2;
+
+ K2->Height = Max (Height (K2->Left), Height (K2->Right)) + 1;
+ K1->Height = Max (Height (K1->Left), K2->Height) + 1;
+
+ return K1; /* New root */
+}
+
+
+/* This function can be called only if K1 has a right child */
+/* Perform a rotate between a node (K1) and its right child */
+/* Update heights, then return new root */
+
+static AvlTree
+SingleRotateWithRight (AvlTree K1)
+{
+ AvlTree K2;
+
+ K2 = K1->Right;
+ K1->Right = K2->Left;
+ K2->Left = K1;
+
+ K1->Height = Max (Height (K1->Left), Height (K1->Right)) + 1;
+ K2->Height = Max (Height (K2->Right), K1->Height) + 1;
+
+ return K2; /* New root */
+}
+
+
+/* This function can be called only if K3 has a left */
+/* child and K3's left child has a right child */
+/* Do the left-right double rotation */
+/* Update heights, then return new root */
+
+static AvlTree
+DoubleRotateWithLeft (AvlTree K3)
+{
+ /* Rotate between K1 and K2 */
+ K3->Left = SingleRotateWithRight (K3->Left);
+
+ /* Rotate between K3 and K2 */
+ return SingleRotateWithLeft (K3);
+}
+
+
+/* This function can be called only if K1 has a right */
+/* child and K1's right child has a left child */
+/* Do the right-left double rotation */
+/* Update heights, then return new root */
+
+static AvlTree
+DoubleRotateWithRight (AvlTree K1)
+{
+ /* Rotate between K3 and K2 */
+ K1->Right = SingleRotateWithLeft (K1->Right);
+
+ /* Rotate between K1 and K2 */
+ return SingleRotateWithRight (K1);
+}
+
+AvlTree
+Insert (AvlTree X, AvlTree T)
+{
+ if (X)
+ {
+
+ if (T == NULL)
+ {
+ T = X;
+ }
+ else
+ {
+ if (X->id < T->id)
+ {
+ T->Left = Insert (X, T->Left);
+ if (Height (T->Left) - Height (T->Right) == 2)
+ {
+ if (X->id < T->Left->id)
+ T = SingleRotateWithLeft (T);
+ else
+ T = DoubleRotateWithLeft (T);
+ }
+ }
+ else if (X->id > T->id)
+ {
+ T->Right = Insert (X, T->Right);
+ if (Height (T->Right) - Height (T->Left) == 2)
+ {
+ if (X->id > T->Right->id)
+ T = SingleRotateWithRight (T);
+ else
+ T = DoubleRotateWithRight (T);
+ }
+ }
+ else
+ printf ("%s déjà inséré ! \n", X->name);
+
+ }
+ T->Height = Max (Height (T->Left), Height (T->Right)) + 1;
+ }
+ return T;
+}
+
+void printAvl(AvlTree T)
+{
+ int i;
+ if (T)
+ {
+ prof++;
+ printAvl(T->Left);
+ for(i=0;i<prof;i++)
+ printf(" ");
+ printf("ID: %i, HEIGHT: %i, NAME: %s, TYPE: %i\n",T->id,T->Height,T->name,T->type);
+ printAvl(T->Right);
+ prof--;
+ }
+}
+
+int getFreshId()
+{
+ count++;
+ return count;
+}
+
+string getName(int X, AvlTree T)
+{
+ AvlTree tmp;
+ tmp= Find(X,T);
+ if (tmp)
+ return tmp->name;
+ else
+ return NULL;
+}
33 avl/avl.h
@@ -0,0 +1,33 @@
+#ifndef _Avl_H
+#define _Avl_H
+#include "../automata/automata.h"
+
+struct AvlNode;
+
+typedef struct AvlNode *AvlTree;
+
+struct AvlNode
+{
+ int id; /* l'id de la location, transition, automate,... */
+ AvlTree Left;
+ AvlTree Right;
+ int Height;
+
+ string name;
+ enum nameType type;
+ union
+ {
+ enum varType vType;/*INTEGRATOR, STOPWATCH, CLOCK, ANALOG, PARAMETER ou DISCRETE*/
+ struct lab * labPtr;
+ struct location *locPtr;
+ struct automaton *automPtr;
+ } data;
+};
+
+AvlTree Find (int X, AvlTree T);
+AvlTree Insert (AvlTree X, AvlTree T);
+AvlTree makeAvlNode(int id, string s, enum nameType ty);
+string getName(int X,AvlTree T);
+int getFreshId();
+void printAvl(AvlTree T);
+#endif /*_AvlTree_H */
5 avl/fatal.h
@@ -0,0 +1,5 @@
+#include <stdio.h>
+#include <stdlib.h>
+
+#define Error( Str ) FatalError( Str )
+#define FatalError( Str ) fprintf( stderr, "%s\n", Str ), exit( 1 )
421 constraints/constraints.c
@@ -0,0 +1,421 @@
+#include "constraints.h"
+
+struct term * makeTerm(int id, struct rational * coeff, enum varStatus status)
+{
+ struct term * res;
+ res= (struct term *) malloc (sizeof(struct term));
+ if (!res)
+ {
+ fprintf(stderr,"Not enough memory!\n");
+ exit(-1);
+ }
+
+ res->id=id;
+ res->coeff=coeff;
+ res->status=status;
+ return res;
+}
+struct term * copyTerm(struct term * data)
+{
+ if (data)
+ return makeTerm(data->id, copyRational(data->coeff), data->status);
+ else
+ return NULL;
+}
+
+
+expr makeExpr(enum exprType type, expr ls, expr rs, struct term * te)
+{
+ expr res;
+ res= (expr) malloc(sizeof(struct exprNode));
+ if (!res)
+ {
+ fprintf(stderr,"Not enough memory!\n");
+ exit(-1);
+ }
+ res->type= type;
+ res->ls=ls;
+ res->rs=rs;
+ res->te=te;
+ return res;
+}
+
+expr copyExpression(expr data)
+{
+ if (data)
+ return makeExpr(data->type,copyExpression(data->ls),
+ copyExpression(data->rs),
+ copyTerm(data->te)
+ );
+ else
+ return NULL;
+}
+
+expr extractInferiorBounds(expr * pe)
+{
+ expr res=NULL;
+ expr e ;
+
+ e= *pe;
+
+ if (e)
+ {
+ switch(e->type)
+ {
+ case AND :
+ {
+ expr ls,rs;
+ ls= extractInferiorBounds(&(e->ls));
+ rs= extractInferiorBounds(&(e->rs));
+ if (ls && rs)
+ res=makeExpr(AND,ls,rs,NULL);
+ else
+ {
+ if (ls)
+ res=ls;
+ else if (rs)
+ res=rs;
+ /*last possibility : res must be set to NULL, nothing to do*/
+ }
+ if (e->ls ==NULL && e->rs==NULL)
+ *pe=NULL;
+ else
+ {
+
+ if(e->ls==NULL)
+ *pe=e->rs;
+ else if (e->rs==NULL)
+ *pe=e->ls;
+ }
+
+ break;
+ }
+ case GEQ :
+ {
+ res=e;
+ *pe=NULL;
+ break;
+ }
+ case GRT :
+ {
+ res=e;
+ *pe=NULL;
+ break;
+ }
+ default : break;
+ }
+ }
+ return res;
+}
+expr DNF(expr e)
+{
+ if (e)
+ {
+ switch(e->type)
+ {
+ case AND :
+ {
+
+ e->ls=DNF(e->ls);
+ e->rs=DNF(e->rs);
+ if (e->ls->type==OR)
+ {
+ expr a,b,c;
+ a=e->ls->ls;
+ b=e->ls->rs;
+ c=e->rs;
+ e->type=OR;
+ e->ls->type=AND;
+ e->ls->rs=c;
+ e->rs=makeExpr(AND,b,copyExpression(c),NULL);
+ }
+ else if (e->rs->type==OR)
+ {
+ expr a,b,c;
+ a=e->ls;
+ b=e->rs->ls;
+ c=e->rs->rs;
+ e->type=OR;
+ e->rs->type=AND;
+ e->rs->ls=a;
+ e->ls=makeExpr(AND,copyExpression(a),b,NULL);
+
+
+ }
+ e->ls=DNF(e->ls);
+ e->rs=DNF(e->rs);
+ break;
+ }
+ case OR :
+ {
+ e->ls=DNF(e->ls);
+ e->rs=DNF(e->rs);
+ break;
+ }
+ default :
+ break;
+ }
+ }
+ return e;
+
+}
+
+
+
+
+bool greaterE(expr A, expr B)
+{
+ if (A && B)
+ switch(A->type)
+ {
+ case TERM :
+ switch (B->type)
+ {
+ case TERM :
+ return (A->te->id==B->te->id && greaterR(A->te->coeff,B->te->coeff));
+ case PLUS :
+ return(greaterE(A,B->ls));
+ break;
+ case MINUS :
+ return(greaterE(A,B->ls));
+ break;
+ default:
+ return 0;
+ }
+ case PLUS :
+ switch(B->type)
+ {
+ case TERM :
+ return(greaterE(A->ls,B));
+ break;
+ case PLUS :
+ return(greaterE(A->ls,B->ls));
+ break;
+ case MINUS :
+ return(greaterE(A->ls,B->ls));
+ break;
+ default :
+ return 0;
+
+ }
+ case MINUS :
+ switch(B->type)
+ {
+ case TERM :
+ return(greaterE(A->ls,B));
+ break;
+ case PLUS :
+ return(greaterE(A->ls,B->ls));
+ break;
+ case MINUS :
+ return(greaterE(A->ls,B->ls));
+ break;
+ default :
+ return 0;
+ }
+ default :
+ return 0;
+ break;
+ }
+ else return 0;
+}
+
+bool imply(expr A, expr B)
+{
+ /* A is a conjunction of inequality, B is an inequality*/
+ if ((A!=NULL && B!=NULL) && A!=B)
+ {
+ switch(A->type)
+ {
+ case LEQ :
+ {
+ if (B->type== LEQ)
+ return(greaterE(B->rs,A->rs));
+ else
+ return 0;
+ break;
+ }
+ case GEQ :
+ {
+ if (B->type== GEQ)
+ return greaterE(A->rs,B->rs);
+ else
+ return 0;
+ break;
+ }
+ case AND :
+ {
+ return(imply(A->ls,B) || imply(A->rs,B));
+ break;
+ }
+ default :
+ {
+ printf("problem \n");
+ return 0;
+ break;
+ }
+ }
+ }
+ else return 0;
+}
+
+
+bool implyConj(expr A, expr B)
+{
+ /* A and B are two conjunctions of inequalities*/
+ if (B && B!=A)
+ {
+ switch(B->type)
+ {
+ case AND :
+ {
+ return(implyConj(A,B->ls)&& implyConj(A,B->rs));
+ break;
+ }
+ default :
+ {
+ return(imply(A,B));
+ break;
+ }
+ }
+
+ }
+ else
+ return 0 ;
+}
+
+bool implyDisj(expr A, expr B)
+{
+ /* A is a conjunction of inequalities,
+ B is a disjunction of conjunction of inequalities*/
+ /*The Function returns true if A implies any of the conjunction of B*/
+ if (B && B!=A)
+ {
+ switch(B->type)
+ {
+ case OR :
+ {
+ return(implyDisj(A,B->ls) || implyDisj(A,B->rs));
+ break;
+ }
+ default:
+ {
+ return(implyConj(A,B));
+ break;
+ }
+ }
+
+ }
+ return 0;
+}
+
+
+
+void simplifyDisjunction(expr * pe, expr * f)
+{
+ bool equalFlag;
+ expr e= *pe;
+ equalFlag=(pe==f);
+
+ if (e)
+ switch(e->type)
+ {
+ case OR :
+ {
+ simplifyDisjunction(&(e->ls),f);
+ if (!(e->ls))
+ {
+ (*pe)=e->rs;
+ if (equalFlag)
+ *f=*pe;
+ simplifyDisjunction(pe,f);
+ }
+ else
+ {
+ simplifyDisjunction(&(e->rs),f);
+ if (!(e->rs))
+ {
+ (*pe)=e->ls;
+ if (equalFlag)
+ *f=*pe;
+ }
+ }
+ break;
+ }
+ default :
+ {
+ simplifyConjunction(pe,pe);
+ if (implyDisj(e,*f))
+ {
+ *pe=NULL;
+ if (equalFlag)
+ *f=*pe;
+ }
+ break;
+ }
+ }
+}
+
+void simplifyConjunction(expr * pe, expr * f)
+{
+ bool equalFlag;
+ expr e= *pe;
+ equalFlag=(pe==f);
+
+ if (e)
+ switch(e->type)
+ {
+ case AND :
+ {
+ simplifyConjunction(&(e->ls),f);
+ if (!(e->ls))
+ {
+ (*pe)=e->rs;
+ if (equalFlag)
+ *f=*pe;
+ simplifyConjunction(pe,f);
+ }
+ else
+ {
+ simplifyConjunction(&(e->rs),f);
+ if (!(e->rs))
+ {
+ (*pe)=e->ls;
+ if (equalFlag)
+ *f=*pe;
+ }
+ }
+ break;
+ }
+ default : /*LES or GEQ*/
+ {
+ if (imply(*f,e))
+ {
+ *pe=NULL;
+ if (equalFlag)
+ *f=*pe;
+ }
+ break;
+ }
+ }
+}
+
+
+/* } */
+
+
+/* expr simplify(expr expression) */
+/* { */
+/* expr res; */
+/* expr temp; */
+/* temp=DNF(expression); */
+
+
+
+
+
+
+
+
+/* return res; */
+/* } */
35 constraints/constraints.h
@@ -0,0 +1,35 @@
+#ifndef __CONSTRAINTS_H
+#define __CONSTRAINTS_H
+#include "../rationals/rationals.h"
+
+
+struct exprNode;
+
+typedef struct exprNode * expr;
+
+struct term
+{
+ int id; /*convention : idVar=-1 signifie que le terme est une constante*/
+ struct rational * coeff;
+ enum varStatus status;
+};
+
+struct exprNode
+{
+ enum exprType type; /*convention : selon le type, on utilise soit ls et rs, soit te, jamais les deux*/
+ struct exprNode * ls;
+ struct exprNode * rs;
+
+ struct term * te;
+};
+
+expr makeExpr(enum exprType type, expr ls, expr rs, struct term * te);
+struct term * makeTerm(int id, struct rational * coeff, enum varStatus status);
+expr extractInferiorBounds(expr *);
+expr copyExpression(expr expression);
+expr DNF(expr expression);
+bool greaterE(expr A, expr B);
+bool imply(expr A, expr B);
+void simplifyConjunction(expr * pe, expr * f);
+void simplifyDisjunction(expr * pe, expr * f);
+#endif
0  constraints/inequalities.h
No changes.
9 constraints/term.h
@@ -0,0 +1,9 @@
+#include "../enum.h"
+#include "../utils/rationals.h"
+typedef int var;
+struct term
+{
+ var v;
+ rational * coeff;
+ enum varStatus status;
+}
0  constraints/terms.h
No changes.
17 enums.h
@@ -0,0 +1,17 @@
+#ifndef __ENUMS_H
+#define __ENUMS_H
+
+enum sign {POSITIVE, NEGATIVE}; /*utilisé dans les rationels*/
+enum varStatus {NORMAL, POST, DERIVATIVE,CONSTANT}; /*utilisé pour désigner le statut d'une variable dans une expression*/
+enum exprType{TERM,LOCINIT,PARAM,
+ TRUE, FALSE,
+ AND, OR,
+ PLUS, MINUS, DIV, TIMES,
+ LES, LEQ, EQU, GEQ, GRT}; /*utilisé dans la définition des expressions*/
+enum varType { INTEGRATOR, STOPWATCH, CLOCK, ANALOG, PARAMETER, DISCRETE, ANY_VAR_TYPE };
+enum nameType {AUTOMATON,LOCATION, LABEL, VAR};/*utilisé dans les AVL*/
+enum labelType {EVENT,ORDER,INTERNAL,STANDARD, BROADCAST, URGENT};
+enum transitionStatus{ORDINARY, ASAP,BROADCASTEMITTER,BROADCASTRECEIVER};
+enum automType {ELASTIC, UPPAAL,HYTECH};
+enum locationType {SLW, URG, COMMIT};
+#endif
118 examples/audio.el
@@ -0,0 +1,118 @@
+-- The Elastic specification of the whole system for the audio control protocol of FM05
+-- Hytech parametric analysis only terminates with stronger constraints than delta1 + delta2 <1/2 *-
+
+
+var
+
+x,y,z : clock;
+i, c,leng, m,p,r,doublezero
+: discrete;
+automaton random
+synclabs : ;
+initially ran & i=0 ;
+
+loc ran : while True wait{}
+ when True do {i'=1} goto ran;
+ when True do {i'=0} goto ran;
+end
+
+
+elastic automaton sender
+
+eventlabs : ;
+internlabs: ;
+orderlabs : up, down;
+
+initially idle & x=0 & p=0 & i=0 & leng=0 & c=0 & doublezero=0;
+
+loc idle :
+ when x>=12 put up do{x'=0,p'=1, c'=1, leng'=1} goto oneSent;
+
+loc oneSent :
+ when x>=2 & x<=2 & i=1 put down do{x'=0} goto waitingOne ;
+ when x>=4 & x<= 4 & i=0 put down do{ x'=0, p'=1-p, leng'=leng+1,c'=2 c,i'>=0,i'<=1,doublezero'=0} goto zeroSent;
+ when x>=2 & x<=2 & p=1 put down do{x'=0,p'=0} goto idle;
+
+loc waitingOne :
+ when x>=2 & x<=2 put up do{x'=0, p'=1-p, leng'=leng+1, c'=2 c +1,i'>=0,i'<=1} goto oneSent;
+
+loc zeroSent :
+ when x>=2 & x<=2 & i=0 put up do {x'=0} goto waitingZero;
+ when x>=4 & x <= 4 & i=1 put up do{ x'=0, p'=1-p, leng'=leng+1, c'=2 c + 1,i'>=0,i'<=1} goto oneSent;
+ when x>=2 & x<=2 & p=1 do{x'=0,p'=0} goto idle;
+ when x>=2 & x<=2 & doublezero=1 do{x'=0, p'=0} goto idle;
+
+
+loc waitingZero :
+ when x>=2 & x<=2 put down do{x'=0, p'=1-p, leng'=leng+1,c'=2 c,i'>=0,i'<=1,doublezero'=1} goto zeroSent;
+end
+
+elastic automaton receiver
+
+eventlabs : up;
+internlabs : finalZero;
+orderlabs : ;
+initially idle2 & y=0 & m=0 & r=0 ;
+
+loc idle2:
+ when get up & True do {y'=0,m'=1,r'=1} goto last_is_1;
+loc last_is_1 :
+ when get up & 3<=y & y<=5 do {y'=0,m'=1-m,r'=1} goto last_is_1;
+ when get up & 5<=y & y<=7 do {y'=0,m'=1-m,r'=0} goto last_is_0;
+ when get up & 7<=y do {y'=0,r'=2} goto last_is_1;
+ when y>=9 & m=1 do {y'=0} goto idle2;
+ when y>=9 & m=0 put finalZero do{y'=0,r'=0,m'=1-m} goto idle2;
+loc last_is_0 :
+ when get up & 3<=y & y<=5 do {y'=0, m'=1-m, r'=0} goto last_is_0;
+ when get up & 5<=y do {y'=0, r'=2} goto last_is_1;
+ when y>=7 put finalZero do {y'=0, r'=0} goto idle2;
+
+end
+
+automaton checkOutput
+
+synclabs : getup , finalZero;
+
+initially check & z=0 & leng=0 & c=0 & doublezero=0 ;
+
+loc check : while True wait{}
+ when True sync getup do {z'=0} goto treating;
+ when True sync finalZero do {z'=0} goto treating;
+ when leng>3 goto cerror;
+ when leng<0 goto cerror;
+
+
+loc treating : while z<=0 wait{}
+ when r=0 & leng=1 & c=1 do{z'=0} goto cerror;
+ when r=0 & leng=1 & c=0 do{leng'=leng-1,z'=0} goto check;
+ when r=0 & leng=2 & c>1 do{z'=0} goto cerror;
+ when r=0 & leng=2 & c<=1 do{leng'=leng-1,z'=0} goto check;
+ when r=0 & leng=3 & c>3 do{z'=0} goto cerror;
+ when r=0 & leng=3 & c<=3 do{leng'=leng-1,z'=0} goto check;
+
+ when r=1 & leng=1 & c=0 do{z'=0} goto cerror;
+ when r=1 & leng=1 & c=1 do{leng'=leng-1,c'=c-1,z'=0} goto check;
+ when r=1 & leng=2 & c<=1 do{z'=0} goto cerror;
+ when r=1 & leng=2 & c>1 do{leng'=leng-1,c'=c-2,z'=0} goto check;
+ when r=1 & leng=3 & c<=3 do{z'=0} goto cerror;
+ when r=1 & leng=3 & c>3 do{leng'=leng-1,c'=c-4,z'=0} goto check;
+
+
+ when r=2 & leng=1 do{z'=0} goto cerror;
+ when r=2 & leng=2 & c=1 do{leng'=0, c'=0,z'=0} goto check;
+ when r=2 & leng=2 & c=0 do{z'=0} goto cerror;
+ when r=2 & leng=2 & c>2 do{z'=0} goto cerror;
+ when r=2 & leng=3 & c=3 do {leng'=1, c'=1,z'=0} goto check;
+ when r=2 & leng=3 & c=2 do {leng'=1,c'=0,z'=0} goto check;
+ when r=2 & leng=3 & c>3 do{z'=0} goto cerror;
+ when r=2 & leng=3 & c<2 do{z'=0} goto cerror;
+
+loc cerror : while True wait{}
+
+end
+
+init := param[sender]= 1/5 & param[receiver]=1/5;
+
+bad := loc[checkOutput] = cerror ;
+
+view[up]=getup;
66 examples/exemple1.el
@@ -0,0 +1,66 @@
+-* simplified example from HSCC04 *-
+-* Hytech parametric analysis only terminate with a non-null inferior bound on the parameter (delta1>1/10) *-
+
+-*--------------------------------------------------------------------
+ Declarations
+--------------------------------------------------------------------*-
+
+define(alpha, 2) -- ou 1
+
+var
+ w, x, y : clock;
+
+
+elastic automaton controller
+
+eventlabs : B;
+internlabs : ;
+orderlabs : A, C;
+
+initially c1 & w=0;
+
+loc c1 :
+ when w>=1 put A do {w' = 0} goto c2;
+loc c2 :
+ when get B & True goto c3;
+loc c3 :
+ when True put C goto c1;
+end
+
+-*--------------------------------------------------------------------
+ Environment
+--------------------------------------------------------------------*-
+
+automaton environment
+
+synclabs: A,
+ B,
+ C;
+initially e1 & x=0 & y=0;
+
+loc e1: while True wait {}
+ when True sync A do {x' = 0} goto e2;
+ when x>=alpha goto Bad;
+ when True sync C goto Bad; -- receptiveness checking
+
+loc e2: while y<=1 wait {}
+ when y>=1 sync B goto e3;
+ when x>=alpha goto Bad;
+
+ when True sync A goto Bad; -- receptiveness checking
+ when True sync C goto Bad; -- receptiveness checking
+
+loc e3: while True wait {}
+ when True sync C do{y'=0} goto e1;
+ when x>=alpha goto Bad;
+
+ when True sync A goto Bad; -- receptiveness checking
+
+loc Bad: while True wait{}
+
+end
+
+
+init := param[controller]=1/5 ;
+
+bad := loc[environment] = Bad ;
73 examples/exemple2.el
@@ -0,0 +1,73 @@
+
+-* Example from HSCC04 *-
+-* Hytech parametric analysis only terminate with a non-null inferior bound on the parameter (delta1>1/10) *-
+
+-*--------------------------------------------------------------------
+ Declarations
+--------------------------------------------------------------------*-
+
+define(alpha, 2) -- ou 1
+
+var
+ t, x, y ,z: clock;
+
+-*--------------------------------------------------------------------
+ Controller
+--------------------------------------------------------------------*-
+
+elastic automaton controleur
+
+eventlabs : B;
+internlabs : ;
+orderlabs : A, C;
+
+initially c1 & t=0 & z=0;
+
+loc c1 :
+ when True put A do {t' = 0} goto c2;
+loc c2 :
+ when get B & t<=3/4 goto c3;
+ when get B & t>=3/4 do{z'=0} goto c4;
+loc c3 :
+ when t>=3/4 do{z'=0} goto c4;
+loc c4 :
+ when True put C do{z'=0} goto c1;
+end
+
+-*--------------------------------------------------------------------
+ Environment
+--------------------------------------------------------------------*-
+
+automaton environment
+
+synclabs: A,
+ B,
+ C;
+initially e1 & x=0 & y=0;
+
+loc e1: while True wait {}
+ when True sync A do {x' = 0} goto e2;
+ when x>alpha goto Bad;
+ when True sync C goto Bad; -- receptiveness checking
+
+loc e2: while y<=1 wait {}
+ when True sync B goto e3;
+ when x>alpha goto Bad;
+
+ when True sync A goto Bad; -- receptiveness checking
+ when True sync C goto Bad; -- receptiveness checking
+
+loc e3: while True wait {}
+ when x>=1/2 sync C do{y'=0} goto e1;
+ when x>alpha goto Bad;
+
+ when True sync A goto Bad; -- receptiveness checking
+ when x<1/2 sync C goto Bad; -- receptivenes checking
+loc Bad: while True wait{}
+
+end
+
+
+
+bad := loc[environment] = Bad ;
+
277 examples/proto2.el
@@ -0,0 +1,277 @@
+-* The philips audio control protocol with 2 senders *-
+-* Only usable with UPPAAL *-
+define(sFreq,1)
+define(bound,8)
+define(boundminusone,7)
+define(Bbound,9)
+define(Bboundminusone,8)
+define(delta,1/8)
+var Ax,z ,y, Bx
+ : clock;
+ Acount, Asending, Astarting, Ac, Aleng, Ap, AdoubleZero, Acol,
+ Bcount, Bstarting, Bp, BdoubleZero,
+ i,Bi,
+ m,r,
+ upi
+ : discrete ;
+
+automaton wire
+synclabs : Aup, Adown, AtestVolt, AVoltYes, AVoltNo, Bup, Bdown, BtestVolt, BVoltYes, BVoltNo, up;
+
+initially isDown & upi=0 ;
+
+loc isDown : while True wait{}
+ when True sync Aup do{upi'=1} goto isUp0;
+ when True sync Bup do{upi'=1} goto isUp0;
+ when True sync AtestVolt goto isDown2;
+ when True sync BtestVolt goto isDown3;
+
+loc isDown2 : while True wait{}
+ when asap sync AVoltNo goto isDown;
+
+loc isDown3 : while True wait{}
+ when asap sync BVoltNo goto isDown;
+
+loc isUp0 : while True wait{}
+ when asap sync up goto isUp;
+
+loc isUp : while True wait{}
+ when upi=1 sync Adown do{upi'=0} goto isDown;
+ when upi>1 sync Adown do{upi'=upi-1} goto isUp;
+ when True sync Aup do{upi'=upi+1} goto isUp;
+
+ when upi=1 sync Bdown do{upi'=0} goto isDown;
+ when upi>1 sync Bdown do{upi'=upi-1} goto isUp;
+ when True sync Bup do{upi'=upi+1} goto isUp;
+
+ when True sync AtestVolt goto isUp2;
+ when True sync BtestVolt goto isUp3;
+
+loc isUp2 : while True wait{}
+ when asap sync AVoltYes goto isUp;
+
+loc isUp3 : while True wait{}
+ when asap sync BVoltYes goto isUp;
+end
+
+
+elastic automaton Asender
+eventlabs : AVoltYes, AVoltNo;
+internlabs : ;
+orderlabs : Aup, Adown, AtestVolt;
+
+initially Aidle & Ax=0 & Asending=0 & Astarting=0 & Acol=0 & Ac=0 & Aleng=0 & AdoubleZero=0 & Acount=0 & Ap=0;
+
+loc Aidle :
+ when Ax>=sFreq put AtestVolt do{Ax'=0} goto Aidle2 ;
+
+loc Aidle2 :
+ when get AVoltYes & True do{Ax'=0, Acount'=0} goto Aidle;
+ when get AVoltNo & Acount<= boundminusone do{Ax'=0, Acount'=Acount+1} goto Aidle;
+ when get AVoltNo & Acount = bound goto Aidle3;
+
+loc Aidle3 :
+ when True put Aup do{Ax'=0, Aleng'=1, Ac'=1, Ap'=1, Acount'=0,Astarting'=1,Asending'=1} goto AoneSent;
+
+loc AoneSent :
+ when Ax>=2 & Ax <=2 & i=1 put Adown do{Ax'=0, Astarting'=0} goto AwaitingOne ;
+ when Ax>=4 & Ax <=4 & i=0 & Astarting=0 put Adown do{ Ax'=0, Ap'=1-Ap, Aleng'=Aleng+1, Ac'=2 Ac,AdoubleZero'=0} goto AzeroSent;
+ when Ax>=2 & Ax <=2 & Ap=1 & Astarting=0 put Adown do{Asending'=0, Ax'=0, Ap'=0} goto Aidle;
+
+loc AwaitingOne :
+ when Ax>=sFreq & Acount<=0 put AtestVolt do{Ax'=0} goto AwaitingOne2;
+ when Ax>=sFreq & Acount=1 put Aup do{Acount'=0,Ax'=0, Ap'=1-Ap, Aleng'=Aleng+1, Ac'=2 Ac+1} goto AoneSent;
+
+loc AwaitingOne2 :
+ when get AVoltYes & True do{Acount'=0,Asending'=0,Ax'=0,Acol'=1} goto Aidle;
+ when get AVoltNo & True do{Acount'=Acount+1, Ax'=0} goto AwaitingOne;
+
+loc AzeroSent :
+ when Ax>=sFreq put AtestVolt do{Ax'=0} goto AzeroSent2;
+
+loc AzeroSent2 :
+ when get AVoltYes & True do{Acount'=0,Asending'=0,Ax'=0,Acol'=1} goto Aidle;
+ when get AVoltNo & True do{Acount'=0, Ax'=0} goto AzeroSent3;
+
+loc AzeroSent3 :
+ when Ax>=sFreq & i=0 put Aup do{Ax'=0} goto AwaitingZero;
+ when Ax>=sFreq & Ax<=sFreq & i=1 do{Ax'=0} goto AzeroSent4;
+ when Ax>=sFreq & Ap=1 do{Asending'=0, Ax'=0, Ap'=0} goto Aidle;
+ when Ax>=sFreq & AdoubleZero=1 do{Asending'=0, Ax'=0, Ap'=0 } goto Aidle;
+
+loc AzeroSent4 :
+ when Ax>=sFreq put AtestVolt do{Ax'=0} goto AzeroSent5 ;
+
+loc AzeroSent5 :
+ when get AVoltYes & True do{Asending'=0,Ax'=0,Acol'=0} goto Aidle;
+ when get AVoltNo & True do{Ax'=0} goto AzeroSent6;
+
+loc AzeroSent6 :
+ when Ax>=sFreq & Ax<=sFreq put Aup do{ Ax'=0, Ap'=1-Ap, Aleng'=Aleng+1,Ac'=2 Ac+1} goto AoneSent;
+
+loc AwaitingZero :
+ when Ax>=2 & Ax<=2 put Adown do{Ax'=0,Ap'=1-Ap,Aleng'=Aleng+1,Ac'=2 Ac,AdoubleZero'=1} goto AzeroSent;
+
+end
+
+elastic automaton Bsender
+eventlabs : BVoltYes, BVoltNo;
+internlabs : ;
+orderlabs : Bup, Bdown, BtestVolt;
+
+initially Bidle & Bx=0 & Bstarting=0 & Bp=0 & Bcount=0 & BdoubleZero=0;
+
+loc Bidle :
+ when Bx>=sFreq put BtestVolt do{Bx'=0} goto Bidle2 ;
+
+loc Bidle2 :
+ when get BVoltYes & True do{Bx'=0, Bcount'=0} goto Bidle;
+ when get BVoltNo & Bcount<= Bboundminusone do{Bx'=0, Bcount'=Bcount+1} goto Bidle;
+ when get BVoltNo & Bcount = Bbound goto Bidle3;
+
+loc Bidle3 :
+ when get Bup & True do{Bx'=0, Bp'=1, Bcount'=0,Bstarting'=1} goto BoneSent;
+
+loc BoneSent :
+ when Bx>=2 & Bi=1 & Bstarting=0 put Bdown do{Bx'=0} goto BwaitingOne ;
+ when Bx>=4 & Bi=0 put Bdown do{ Bx'=0, Bp'=1-Bp, BdoubleZero'=0, Bstarting'=0} goto BzeroSent;
+ when Bx>=2 & Bp=1 & Bstarting=0 put Bdown do{Bx'=0, Bp'=0} goto Bidle;
+
+loc BwaitingOne :
+ when Bx>=sFreq & Bcount<=0 put BtestVolt do{Bx'=0} goto BwaitingOne2;
+ when Bx>=sFreq & Bcount=1 put Bup do{Bcount'=0,Bx'=0, Bp'=1-Bp} goto BoneSent;
+
+loc BwaitingOne2 :
+ when get BVoltYes & True do{Bcount'=0,Bx'=0} goto Bidle;
+ when get BVoltNo & True do{Bcount'=Bcount+1, Bx'=0} goto BwaitingOne;
+
+loc BzeroSent :
+ when Bx>=sFreq put BtestVolt do{Bx'=0} goto BzeroSent2;
+
+loc BzeroSent2 :
+ when get BVoltYes & True do{Bcount'=0,Bx'=0} goto Bidle;
+ when get BVoltNo & True do{Bcount'=0, Bx'=0} goto BzeroSent3;
+
+loc BzeroSent3 :
+ when Bx>=sFreq & Bi=0 put Bup do{Bx'=0} goto BwaitingZero;
+ when Bx>=sFreq & Bi=1 do{Bx'=0} goto BzeroSent4;
+ when Bx>=sFreq & Bp=1 do{Bx'=0, Bp'=0 } goto Bidle;
+ when Bx>=sFreq & BdoubleZero=1 do{Bx'=0, Bp'=0 } goto Bidle;
+
+loc BzeroSent4 :
+ when Bx>=sFreq put BtestVolt do{Bx'=0} goto BzeroSent5 ;
+
+loc BzeroSent5 :
+ when get BVoltYes & True do{Bx'=0} goto Bidle;
+ when get BVoltNo & True do{Bx'=0} goto BzeroSent6;
+
+loc BzeroSent6 :
+ when Bx>=sFreq put Bup do{ Bx'=0, Bp'=1-Bp} goto BoneSent;
+
+
+loc BwaitingZero :
+ when Bx>=2 put Bdown do{Bx'=0,Bp'=1-Bp,BdoubleZero'=1} goto BzeroSent;
+
+end
+
+elastic automaton receiver
+
+eventlabs : up;
+internlabs : finalZero, endMsg;
+orderlabs : ;
+
+initially idle2 & y=0 & m = 0 & r = 0 ;
+
+loc idle2 :
+ when get up & True do{y' = 0 , m' = 1 , r' = 1 } goto last_is_1;
+
+loc last_is_1 :
+ when get up & y >= 3 & y <= 5 do{y' = 0 , m' = 1 - m , r' = 1 } goto last_is_1;
+ when get up & y >= 5 & y <= 7 do{y' = 0 , m' = 1 - m , r' = 0 } goto last_is_0;
+ when get up & y >= 7 do{y' = 0 , r' = 2 } goto last_is_1;
+ when y >= 9 & m = 1 put endMsg do{y' = 0 } goto idle2;
+ when y >= 9 & m = 0 put finalZero do{y' = 0 , r' = 0 , m' = 1 - m } goto idle2;
+
+loc last_is_0 :
+ when get up & y >= 3 & y <= 5 do{y' = 0 , m' = 1 - m , r' = 0 } goto last_is_0;
+ when get up & y >= 5 do{y' = 0 , r' = 2 } goto last_is_1;
+ when y >= 7 put finalZero do{y' = 0 , r' = 0 } goto idle2;
+end
+
+automaton checkOutput
+synclabs : getup, finalZero, endMsg;
+
+initially checkIdle & z = 0 & Aleng = 0 & Ac = 0 & AdoubleZero = 0 ;
+
+loc checkIdle : while True wait{}
+ when Asending=1 sync getup do{z' = 0 } goto treating;
+ when Asending=0 sync getup do{z'=0,Ac'=0, Aleng'=0} goto checkIdle;
+
+ when True sync finalZero do{z'=0, Aleng'=0, Ac'=0} goto checkIdle ;
+ when True sync endMsg do{z'=0, Aleng'=0, Ac'=0} goto checkIdle ;
+
+loc check : while True wait{}
+
+ when True sync getup do{z'=0} goto treating;
+
+ when Aleng=1 & Ac=0 sync finalZero do {Aleng'=0} goto checkIdle;
+
+ when Aleng=0 sync finalZero do {Aleng'=0, Ac'=0} goto cerror;
+ when Aleng>1 sync finalZero do {Aleng'=0, Ac'=0} goto cerror;
+ when Ac>0 sync finalZero do{Aleng'=0, Ac'=0} goto cerror;
+
+ when Aleng = 0 sync endMsg do{Aleng'=0, Ac'=0} goto checkIdle;
+ when Aleng >0 sync endMsg do{Aleng'=0, Ac'=0} goto cerror;
+
+loc treating : while z <= 0 wait{}
+ when Aleng <=0 do{z'=0} goto cerror;
+ when r = 0 & Aleng = 1 & Ac = 1 do{z' = 0 } goto cerror;
+ when r = 0 & Aleng = 1 & Ac = 0 do{Aleng' = Aleng - 1 , z' = 0 } goto check;
+ when r = 0 & Aleng = 2 & Ac > 1 do{z' = 0 } goto cerror;
+ when r = 0 & Aleng = 2 & Ac <= 1 do{Aleng' = Aleng - 1 , z' = 0 } goto check;
+ when r = 0 & Aleng = 3 & Ac > 3 do{z' = 0 } goto cerror;
+ when r = 0 & Aleng = 3 & Ac <= 3 do{Aleng' = Aleng - 1 , z' = 0 } goto check;
+ when r = 1 & Aleng = 1 & Ac = 0 do{z' = 0 } goto cerror;
+ when r = 1 & Aleng = 1 & Ac = 1 do{Aleng' = Aleng - 1 , Ac' = Ac - 1 , z' = 0 } goto check;
+ when r = 1 & Aleng = 2 & Ac <= 1 do{z' = 0 } goto cerror;
+ when r = 1 & Aleng = 2 & Ac > 1 do{Aleng' = Aleng - 1 , Ac' = Ac - 2 , z' = 0 } goto check;
+ when r = 1 & Aleng = 3 & Ac <= 3 do{z' = 0 } goto cerror;
+ when r = 1 & Aleng = 3 & Ac > 3 do{Aleng' = Aleng - 1 , Ac' = Ac - 4 , z' = 0 } goto check;
+ when r = 2 & Aleng = 1 do{z' = 0 } goto cerror;
+ when r = 2 & Aleng = 2 & Ac = 1 do{Aleng' = 0 , Ac' = 0 , z' = 0 } goto check;
+ when r = 2 & Aleng = 2 & Ac = 0 do{z' = 0 } goto cerror;
+ when r = 2 & Aleng = 2 & Ac > 2 do{z' = 0 } goto cerror;
+ when r = 2 & Aleng = 3 & Ac = 3 do{Aleng' = 1 , Ac' = 1 , z' = 0 } goto check;
+ when r = 2 & Aleng = 3 & Ac = 2 do{Aleng' = 1 , Ac' = 0 , z' = 0 } goto check;
+ when r = 2 & Aleng = 3 & Ac > 3 do{z' = 0 } goto cerror;
+ when r = 2 & Aleng = 3 & Ac < 2 do{z' = 0 } goto cerror;
+
+loc cerror : while z<=6 wait{}
+ when True sync getup do {Aleng'=0, Ac'=0} goto cerror;
+ when True sync finalZero do{Aleng'=0,Ac'=0} goto cerror;
+ when True sync endMsg do{Aleng'=0, Ac'=0} goto cerror;
+
+ when z>=6 & Acol=0 do{z'=0} goto cerror2;
+ when z>=6 & Acol=1 do{Acol'=0, Aleng'=0, Ac'=0,z'=0} goto checkIdle;
+
+loc cerror2 : while z<=0 wait{}
+ when True goto cerror2;
+end
+
+automaton random
+synclabs : ;
+
+initially ran & i = 0 & Bi = 0 ;
+
+loc ran : while True wait{}
+ when True do{i' = 1 } goto ran;
+ when True do{i' = 0 } goto ran;
+ when True do{Bi' = 1 } goto ran;
+ when True do{Bi' = 0 } goto ran;
+end
+
+init := param[Asender]=delta & param[Bsender]=delta & param[receiver]=delta ;
+
+bad := loc[checkOutput] = cerror2 ;
+
+view[up]=getup;
189 main.c
@@ -0,0 +1,189 @@
+#include <stdio.h>
+#include <stdlib.h>
+#include <string.h>
+#include <unistd.h>
+#include "parser/parser.h"
+#include "writeUppaal/writeUppaal.h"
+#include "toUppaal/toUppaal.h"
+
+typedef struct InputParameters{
+ int languageToProduce;
+ bool receptivenessChecking ;
+ /* 0 : Uppaal , 1 : HyTech (DEFAULT) */
+}InputParameters;
+
+
+InputParameters * analyseInputParameters(int paramNumber, char **textParam){
+ /* traitement des paramètres fournis à notre programme. Cette fonction analyse les
+ <paramNumber> paramètres stockés dans <textParam> et retourne la configuration
+ définie par ces paramètres */
+ InputParameters * result;
+ int i;
+ /* vérification des paramètres */
+ if (textParam == NULL){
+ fprintf(stderr, "function analyseInputParameters error ! The parameter 'textParam' can't be NULL.\n");
+ exit(-1);
+ }
+ /* fin vérification des paramètres */
+ result = (InputParameters *)malloc(sizeof(InputParameters));
+ result->languageToProduce=0;
+ result->receptivenessChecking=0;
+ for (i = 1 ; i < paramNumber ; i++){
+ if (strcmp(textParam[i], "-H") == 0){
+ result->languageToProduce = 0;
+ }else if (strcmp(textParam[i], "-U") == 0){
+ result->languageToProduce = 1;
+ }
+ else if (strcmp(textParam[i], "-R")==0)
+ {
+ result->receptivenessChecking=1;
+ }
+ else{
+ fprintf(stderr, "- Warning : unknown option \"%s\". Ignored.\n", textParam[i]);
+ }
+ }
+ return result;
+}
+
+void printToolUsage(){
+ /* affiche les différentes options avec lesquelles notre programme peut être lancé */
+ printf("Tool for translating Elastic specifications to Hytech or Uppaal language\n");
+ printf("Usage: elastic [-options] <filename>\n");
+ printf("\t[-H/-U]\t translation option\n");
+ printf("\t\t H : Elastic to HyTech language [def], \n\t\t U : Elastic to Uppaal language.\n");
+ printf("\t[-R] receptiveness checking for controllers\n");
+}
+
+string makeOutputFileName(string inputFileName, int languageToProduce){
+ /* a partir du langage d'ouput défini par <languageToProduce> et du nom <inputFileName>
+ représentant le fichier d'input, construit et retourne le nom du fichier d'output */
+ string outputFileName;
+ int slashPosition = -1;
+ int pointPosition = -1;
+ int i;
+ /* vérification des paramètres */
+ if (inputFileName == NULL){
+ fprintf(stderr, "function makeOutputFileName error ! The parameter 'inputFileName' can't be NULL.\n");
+ exit(-1);
+ }
+ /* fin vérification des paramètres */
+ for (i = 0 ; i < strlen(inputFileName) ; i++){
+ if (inputFileName[i] == '/'){
+ slashPosition = i;
+ }else if (inputFileName[i] == '.'){
+ pointPosition = i;
+ }
+ }
+ /* SI : nom input = "directory/fileName" ou "fileName" */
+ if (pointPosition <= slashPosition){
+ /* SI : langage = Uppaal */
+ if (languageToProduce == 1 || languageToProduce==2){
+ outputFileName = (char *)malloc(sizeof(char) *(strlen(inputFileName) + 1));
+ strcpy(outputFileName, inputFileName);
+ }
+ /* SINON : langage = Hytech */
+ else{
+ outputFileName = (char *)malloc(sizeof(char) *(strlen(inputFileName) + 6));
+ strcpy(outputFileName, inputFileName);
+ strcat(outputFileName, ".hy\0");
+ }
+ }
+ /* SINON : nom input = "directory/fileName.ext" ou "fileName.ext" */
+ else{
+ /* SI : langage = Uppaal */
+ if (languageToProduce == 1 || languageToProduce==2){
+ outputFileName = (char *)malloc(sizeof(char) * (pointPosition + 1));
+ strncpy(outputFileName, inputFileName, pointPosition);
+ }
+ /* SINON : langage = Hytech */
+ else{
+ outputFileName = (char *)malloc(sizeof(char) * (pointPosition + 6));
+ strncpy(outputFileName, inputFileName, pointPosition);
+ strcat(outputFileName, ".hy\0");
+ }
+ }
+ return outputFileName;
+}
+
+
+void systemTreatment(InputParameters *inputParam, string outputFileName){
+ /* l'arbre de parsing préalablement construit, cette fonction va lui appliquer les
+ différentes transformations précisées par <inputParam>, puis générer le fichier
+ d'ouput nommé <outputFileName> */
+ /* vérification des paramètres */
+ string tmp;
+ struct system * syst;
+ if (inputParam == NULL){
+ fprintf(stderr, "function systemTreatment error ! The parameter 'inputParam' can't be NULL.\n");
+ exit(-1);
+ }
+ if (outputFileName == NULL){
+ fprintf(stderr, "function systemTreatment error ! The parameter 'outputFileName' can't be NULL.\n");
+ exit(-1);
+ }
+ /* fin vérification des paramètres */
+ syst= getSystem();
+
+ syst->receptivenessChecking=inputParam->receptivenessChecking;
+ if (inputParam->languageToProduce==1)
+ {
+ toWatchers(syst);
+ toUppaal(syst);
+ writeUppaal(syst,outputFileName);
+ }
+ else if (inputParam->languageToProduce==0)
+ {
+ toWatchers(syst);
+ writeHyTech(syst,outputFileName);
+ }
+ else
+ {
+ toUppaal(syst);
+ writeUppaal(syst,outputFileName);
+ }
+
+
+}
+
+int main(int argc, char **argv){
+
+
+ FILE *idFile;
+ InputParameters *inputParam;
+ if (argc == 1
+ || (argc == 2 && (strcmp(argv[1], "-H") == 0 ||strcmp(argv[1], "-U") == 0 ||strcmp(argv[1], "-HU") == 0 ) )){
+ printToolUsage();
+ }else{
+ inputParam = analyseInputParameters(argc - 1, argv);
+ idFile = fopen(argv[argc - 1], "r");
+ if (idFile != NULL){
+ setInputPreProc(idFile);
+ setOutputPreProc("tmpInput");
+ if (ppparse() == 1){
+ printf("- Error : incorrect input.\n");
+ unlink("tmpInput");
+ fclose(idFile);
+ }
+ else{
+ setInputParser("tmpInput");
+ if (yyparse() == 1){
+ printf("- Error : incorrect input.\n");
+ unlink("tmpInput");
+ fclose(idFile);
+ }
+ else{
+ string outputFileName;
+ printf("- Correct Input.\n");
+ unlink("tmpInput");
+ fclose(idFile);
+ outputFileName = makeOutputFileName(argv[argc - 1], inputParam->languageToProduce);
+ systemTreatment(inputParam, outputFileName);
+ }
+ }
+ }else{
+ fprintf(stderr, "- Erreur : ouverture du fichier \"%s\" echouee.\n", argv[argc - 1]);
+ exit(-1);
+ }
+ }
+ return 0;
+}
86 makefile
@@ -0,0 +1,86 @@
+FLAGS= -g
+
+elastic : rationals.o utils.o constraints.o toUppaal.o toWatchers.o labStatus.o rationalTreatment.o automata.o avl.o lex.yy.o parser.tab.o preProcessing.tab.o lex.pp.o writeUppaal.o writeHyTech.o tableOfConstants.o system.o enums.h
+ gcc $(FLAGS) -o elastic main.c rationals.o utils.o toUppaal.o toWatchers.o labStatus.o constraints.o rationalTreatment.o automata.o avl.o lex.yy.o parser.tab.o preProcessing.tab.o writeUppaal.o writeHyTech.o lex.pp.o tableOfConstants.o system.o
+
+lex.pp.o : lex.pp.c
+ gcc $(FLAGS) -c -pedantic lex.pp.c
+
+toUppaal.o : toUppaal/toUppaal.c toUppaal/toUppaal.h
+ gcc $(FLAGS) -c -pedantic -Wall toUppaal/toUppaal.c
+
+toWatchers.o : toWatchers/toWatchers.c toWatchers/toWatchers.h
+ gcc $(FLAGS) -c -pedantic -Wall toWatchers/toWatchers.c
+
+preProcessing.tab.o : preProcessing.tab.c
+ gcc $(FLAGS) -c -pedantic -Wall preProcessing.tab.c
+
+tableOfConstants.o : preProcessing/tableOfConstants.c preProcessing/tableOfConstants.h
+ gcc $(FLAGS) -c -pedantic -Wall preProcessing/tableOfConstants.c
+
+rationals.o : rationals/rationals.c rationals/rationals.h
+ gcc $(FLAGS) -c -pedantic -Wall rationals/rationals.c
+
+labStatus.o : utils/labStatus.c utils/labStatus.h
+ gcc $(FLAGS) -c -pedantic -Wall utils/labStatus.c
+
+utils.o : utils/utils.c utils/utils.h
+ gcc $(FLAGS) -c -pedantic -Wall utils/utils.c
+
+rationalTreatment.o : toUppaal/rationalTreatment.h toUppaal/rationalTreatment.c
+ gcc $(FLAGS) -c -pedantic -Wall toUppaal/rationalTreatment.c
+
+constraints.o : constraints/constraints.c constraints/constraints.h
+ gcc $(FLAGS) -c -pedantic -Wall constraints/constraints.c
+
+system.o : system/system.h system/system.c
+ gcc $(FLAGS) -c -pedantic -Wall system/system.c
+
+automata.o : automata/automata.h automata/automata.c
+ gcc $(FLAGS) -c -pedantic -Wall automata/automata.c
+
+writeUppaal.o : writeUppaal/writeUppaal.h writeUppaal/writeUppaal.c
+ gcc $(FLAGS) -c -pedantic -Wall writeUppaal/writeUppaal.c
+
+writeHyTech.o : writeHyTech/writeHyTech.h writeHyTech/writeHyTech.c
+ gcc $(FLAGS) -c -pedantic -Wall writeHyTech/writeHyTech.c
+
+avl.o : avl/avl.h avl/avl.c
+ gcc $(FLAGS) -c -pedantic -Wall avl/avl.c
+
+lex.yy.o : lex.yy.c
+ gcc $(FLAGS) -c -pedantic lex.yy.c
+
+parser.tab.o : parser.tab.c
+ gcc $(FLAGS) -c -pedantic -Wall parser.tab.c
+
+lex.yy.c : scanner/scanner.lex parser.tab.c
+ flex scanner/scanner.lex
+
+parser.tab.c : parser/parser.y parser/parser.h
+ bison -d parser/parser.y
+ @if [ -e ./parser/parser.tab.c ]; \
+ then \
+ mv parser/parser.tab.c parser/parser.tab.h . ; \
+ fi
+
+lex.pp.c : preProcessing/preProcessing.lex preProcessing.tab.c
+ flex -Ppp preProcessing/preProcessing.lex
+
+preProcessing.tab.c : preProcessing/preProcessing.y preProcessing/preProcessing.h
+ bison -d -p pp preProcessing/preProcessing.y
+ @if [ -e ./preProcessing/preProcessing.tab.c ]; \
+ then \
+ mv preProcessing/preProcessing.tab.c preProcessing/preProcessing.tab.h . ; \
+ fi
+
+clean :
+ rm -f *.o elastic lex.pp.c lex.yy.c parser.tab.c parser.tab.h preProcessing.tab.c preProcessing.tab.h
+
+cleanOld :
+ rm -f *~
+
+tgz :
+ make clean
+ make cleanOld
+ (cd .. ; tar -czvf elastic.tgz elastic/ )
16 parser/parser.h
@@ -0,0 +1,16 @@
+
+#ifndef __PARSER_H
+#define __PARSER_H
+
+
+
+
+int yyparse();
+/* procède à la construction de l'arbre de parsing à partir du fichier d'input */
+
+void setInputParser(char * tempFileName);
+/* précise que la construction de l'arbre de parsing se fera à partir du contenu
+ du fichier <tempFileName> */
+
+struct system * getSystem();
+#endif
1,413 parser/parser.y
@@ -0,0 +1,1413 @@
+%{
+#include <stdlib.h>
+#include <stdio.h>
+#include <string.h>
+#include <stdio.h>
+#include "parser/parser.h"
+#include "utils/utils.h"
+#include "avl/avl.h"
+#include "enums.h"
+#include "constraints/constraints.h"
+#include "automata/automata.h"
+#include "system/system.h"
+#define YYERROR_VERBOSE
+#define YYMAXDEPTH 1000000
+ int yyerror(char *s);
+ int yylex ();
+
+ extern int yylineno;
+ FILE * yyin;
+
+ int flagASAP=0;
+ struct exprNode * exprTmp3=NULL;
+ struct exprNode * exprTmp4=NULL;
+ int idLabTmp=-1;
+ int idLabTmp2=-1;
+ struct system * syst;
+
+ struct automaton * autom=NULL;
+
+
+ struct stringElem * idLabList=NULL;/* already declared labels*/
+ struct stringElem * idVarList= NULL; /*already declared variables*/
+ struct stringElem * idAutomList=NULL; /*already declared automaton*/
+ struct stringElem * idLocList=NULL; /*already declared locations*/
+
+ struct stringElem * se=NULL;
+ struct stringElem * destList=NULL;
+
+ enum labelType labTy=STANDARD;
+%}
+
+%union {
+ char * text;
+ struct exprNode * expression;
+ int intgr;
+ struct location * loc;
+ struct lab * label;
+ struct rational * signedRational;
+ struct stringElem * stringList;
+ struct transition * trans;
+};
+
+
+/*
+conventions typographiques utilisées
+************************************
+
+- Tous les noms de lexèmes se terminent par le symbole '_' (ce pour éviter que leur nom soit
+ identique à celui d'éventuelles constantes déclarées dans les fichiers liés par 'include').
+- Les noms de lexèmes "mots réservés" sont écrits en majuscules.
+- Les noms de lexèmes "génériques" sont écrits en minuscules.
+- Les noms de règles sont écrits en minuscules. S'ils sont composés de plusieurs mots,
+ ceux sont séparés par le symbole '_' .
+*/
+
+
+/* règles utilisées la déclaration de variables et d'automates */
+%type <text> id_
+%type <intgr> positive_integer_
+
+/* règles utilisées la définition d'automates élastic */
+%type <text> code_lego codeLego_
+%type <intgr> op var_type elastic_event_synchro elastic_order_synchro
+
+%type <signedRational> pos_rational
+%type <stringList> var_list
+%type <loc> elastic_location elastic_locations
+%type <trans> elastic_transition elastic_transitions
+%type <label> elastic_sync_labels elastic_sync_var_nonempty_list elastic_sync_var_list
+%type <expression> elastic_rectangular_constraint elastic_rectangular_predicate
+%type <expression> pos_rational_addition elastic_update_var elastic_update_list
+%type <expression> elastic_update_nonempty_list updates update_list
+%type <expression> init_expr bad_var bad_loc bad_expr
+
+/* règles utilisées la définition d'automates hybrides */
+%type <label> sync_var_noempty_list sync_var_list sync_labels
+%type <loc> location locations
+%type <trans> transition transitions
+%type <expression> state_initialization
+%type <expression> update_linear_term rate_info_list linear_expression
+%type <expression> linear_term convex_predicate linear_constraint
+%type <expression> update_linear_expression update update_nonempty_list
+%type <intgr> relop rate_relop syn_label
+%type <signedRational> rational integer
+
+
+/* les lexèmes */
+%token SYSTEM_ DEFINE_ VAR_ INTEGRATOR_ STOPWATCH_ CLOCK_ ANALOG_ PARAMETER_ DISCRETE_ ELASTIC_AUTOMATON_ END_ INITIALLY_ EVENTLABS_ INTERNLABS_ ORDERLABS_ LOC_ WHEN_ GOTO_ GET_ TRUE_ PUT_ DO_ AUTOMATON_ SYNCLABS_ WHILE_ WAIT_ IN_ SYNC_ FALSE_ ASAP_ LES_ LEQ_ EQU_ GEQ_ GRT_ DELTA_ codeLego_ id_ positive_integer_ ASSIGN_ PARAM_ BAD_ INIT_ VIEW_
+
+%%
+
+parse_tree :
+automata_descriptions system tools_commands
+{
+ fclose(yyin);
+}
+;
+
+system :
+SYSTEM_ automaton_list ';'
+{;}
+|
+{}
+;
+
+automaton_list :
+id_ ',' automaton_list
+{
+
+}
+|
+id_
+{
+
+}
+;
+
+tools_commands :
+init bad couple
+|
+init bad
+|
+init couple
+|
+bad couple
+|
+init
+|
+bad
+|
+couple
+|
+
+;
+
+init :
+INIT_ ASSIGN_ init_expr ';'
+{ syst->paramInit=$3;}
+|
+INIT_ ASSIGN_ ';'
+;
+
+init_expr :
+PARAM_ '[' id_ ']' EQU_ rational
+{
+ int tmpId;
+
+ tmpId=getId($3,idAutomList);
+ if (tmpId==-1)
+ yyerror("Error: Automaton not declared. \n");
+ $$=makeExpr(EQU,
+ makeExpr(PARAM,
+ NULL,
+ NULL,
+ makeTerm(tmpId,makeRational(POSITIVE,1,1),NORMAL)),
+ makeExpr(TERM,
+ NULL,
+ NULL,
+ makeTerm(-1,$6,CONSTANT)),
+ NULL) ;
+
+}
+|
+PARAM_ '[' id_ ']' EQU_ rational '&' init_expr
+{
+ int tmpId;
+
+ tmpId=getId($3,idAutomList);
+ if (tmpId==-1)
+ yyerror("Error: Automaton not declared. \n");
+ $$=makeExpr(AND,
+ makeExpr(EQU,
+ makeExpr(PARAM,
+ NULL,
+ NULL,
+ makeTerm(tmpId,NULL,NORMAL)),
+ makeExpr(TERM,
+ NULL,
+ NULL,
+ makeTerm(-1,$6,CONSTANT)),
+ NULL),
+ $8,
+ NULL);
+}
+;
+
+bad :
+BAD_ ASSIGN_ bad_expr ';'
+{
+ syst->badStates=$3;
+}
+|
+BAD_ ASSIGN_ ';'
+;
+
+bad_expr :
+bad_loc
+{$$=$1;}
+|
+bad_var
+{$$=$1;}
+|
+bad_loc'&' bad_expr
+{
+ $$=makeExpr(AND,$1,$3,NULL);
+}
+|
+bad_loc'|' bad_expr
+{
+ $$=makeExpr(OR,$1,$3,NULL);
+}
+|
+bad_var '&' bad_expr
+{
+ $$=makeExpr(AND,$1,$3,NULL);
+}
+|
+bad_var '|' bad_expr
+{
+ $$=makeExpr(OR,$1,$3,NULL);
+}
+|
+'(' bad_expr ')'
+{
+ $$=$2;
+}
+;
+
+bad_loc :
+LOC_ '[' id_ ']' EQU_ id_
+{
+ int tmpId;
+ int tmpId2;
+
+ tmpId=getId($3,idAutomList);
+ if (tmpId==-1)
+ yyerror("Error: Automaton not declared. \n");
+ tmpId2=getId($6,idLocList);
+ if (tmpId2==-1)
+ yyerror("Error: Target location not declared. \n");
+ $$=makeExpr(LOCINIT,NULL,NULL,makeTerm(tmpId,NULL,tmpId2));
+
+}
+;
+bad_var :
+id_ EQU_ rational
+{
+ int tmpId;
+
+ tmpId=getId($1,idVarList);
+ if (tmpId==-1)
+ yyerror("Error: Variable not declared. \n");
+ $$=makeExpr(EQU,
+ makeExpr(TERM,
+ NULL,
+ NULL,
+ makeTerm(tmpId,makeRational(POSITIVE,1,1),NORMAL)
+ ),
+ makeExpr(TERM,
+ NULL,
+ NULL,
+ makeTerm(-1,$3,NORMAL)
+ ),
+ NULL);
+}
+;
+
+couple :
+ couple_expr ';'
+;
+
+couple_expr :
+VIEW_ '[' id_ ']' EQU_ id_
+{
+ int tmpId;
+ int tmpId2;
+
+ tmpId=getId($3,idLabList);
+ if (tmpId==-1)
+ yyerror("Error: Label not declared. \n");
+ tmpId2=getId($6,idLabList);
+ if (tmpId==-1)
+ yyerror("Error: Label not declared. \n");
+ syst->viewList=makeLabStatus(tmpId,tmpId2,syst->viewList);
+}
+|
+VIEW_ '[' id_ ']' EQU_ id_ '&' couple_expr
+{
+ int tmpId;
+ int tmpId2;
+ tmpId=getId($3,idLabList);
+ if (tmpId==-1)
+ yyerror("Error: Label not declared. \n");
+ tmpId2=getId($6,idLabList);
+ if (tmpId==-1)
+ yyerror("Error: Label not declared. \n");
+ syst->viewList=makeLabStatus(tmpId,tmpId2,syst->viewList);
+}
+;
+
+automata_descriptions :
+declarations automata
+{
+
+}
+;
+
+declarations :
+VAR_ var_lists
+{
+
+}
+;
+
+var_lists :
+var_list ':' var_type ';' var_lists
+{
+ idVarList=appendStringList(idVarList,$1);
+ for(se=$1;se!=NULL;se=se->next)
+ {
+ /*d'abord, insertion de la clef dans le dictionnaire*/
+ AvlTree tmp=makeAvlNode(se->id,se->s,VAR);
+ tmp->data.vType=$3;
+ syst->idDic=Insert(tmp, syst->idDic);
+ /*insertion de la variable dans la liste des variables du système*/
+ syst->varList=makeVar(se->id,syst->varList);
+ }
+}
+|
+':' var_type ';' var_lists
+{
+
+}
+|
+{
+
+}
+;
+
+var_list :
+id_ ',' var_list
+{
+ $$=insertStringElem($1,getFreshId(),$3);
+}
+|
+id_
+{
+ $$=insertStringElem($1,getFreshId(),NULL);
+}
+;
+
+var_type :
+INTEGRATOR_
+{
+ $$=INTEGRATOR;
+}
+|
+STOPWATCH_
+{
+ $$=STOPWATCH;
+}
+|
+CLOCK_
+{
+ $$=CLOCK;
+}
+|
+ANALOG_
+{
+ $$=ANALOG;
+}
+|
+PARAMETER_
+{
+ $$=PARAMETER;
+}
+|
+DISCRETE_
+{
+ $$=DISCRETE;
+}
+;
+
+automata :
+automaton automata
+{
+
+}
+|
+automaton
+{
+
+}
+;
+
+automaton :
+ELASTIC_AUTOMATON_ id_ elastic_sync_labels initialization elastic_locations END_
+{
+ int tmpId;
+ idAutomList=insertStringElem($2,getFreshId(),idAutomList);
+ tmpId=getId($2,idAutomList);
+ syst->automList=makeAutomaton(tmpId,ELASTIC,exprTmp4,idLabTmp2,$3,$5,syst->automList);
+ syst->idDic=Insert(makeAvlNode(tmpId,$2,AUTOMATON),syst->idDic);
+ /*printStringList(idList);*/
+ while (destList!=NULL)
+ {
+ if (getId(destList->s,idLocList)==-1)
+ yyerror("One of the transition destinations does not exist!\n");
+ destList=destList->next;
+ }
+}
+|
+AUTOMATON_ id_ sync_labels initialization locations END_
+{ int tmpId;
+ idAutomList=insertStringElem($2,getFreshId(),idAutomList);
+ tmpId=getId($2,idAutomList);
+ syst->automList=makeAutomaton(tmpId,HYTECH,exprTmp4,idLabTmp2,$3,$5,syst->automList);
+ syst->idDic=Insert(makeAvlNode(tmpId,$2,AUTOMATON),syst->idDic);
+ /*printStringList(idList);*/
+ while (destList!=NULL)
+ {
+ if (getId(destList->s,idLocList)==-1)
+ yyerror("One of the transition destinations does not exist!\n");
+ destList=destList->next;
+ }
+}
+;
+
+/* elastic_initialization : */
+/* INITIALLY_ id_ ';' */
+/* { */
+/* int tmpId; */
+/* tmpId=getId($2,idLocList); */
+
+/* if (tmpId==-1)/*la location n'a pas encore été déclarée */
+/* { */
+/* destList=insertStringElem($2,getFreshId(),destList); */
+/* tmpId=getId($2,destList); /*on vérifiera + tard si la location existe vraiment */
+/* } */
+/* $$=tmpId; */
+/* } */
+/* ; */
+
+elastic_sync_labels :
+EVENTLABS_ ':' {labTy=EVENT; } elastic_sync_var_list ';'
+INTERNLABS_ ':' {labTy=INTERNAL; } elastic_sync_var_list ';'
+ORDERLABS_ ':' {labTy=ORDER; } elastic_sync_var_list ';'
+{
+ $$=appendLabList($4,appendLabList($9,$14));
+}
+;
+
+elastic_sync_var_list :
+elastic_sync_var_nonempty_list
+{
+ $$=$1;
+}
+|
+{
+ $$=NULL;
+}
+;
+
+elastic_sync_var_nonempty_list :
+id_ ',' elastic_sync_var_nonempty_list
+{
+ int tmpId;
+ struct lab * labTmp;
+ AvlTree tmp;
+ tmpId=getId($1,idLabList);
+
+ if (tmpId==-1)
+ {
+ idLabList=insertStringElem($1,getFreshId(),idLabList);
+ tmpId= getId($1,idLabList);
+ labTmp=makeLabel(tmpId,labTy,$3);
+ tmp=makeAvlNode(tmpId,$1,LABEL);
+ tmp->data.labPtr=labTmp;
+ syst->idDic=Insert(tmp, syst->idDic);
+ }
+ else
+ labTmp=makeLabel(tmpId,labTy,$3);
+ $$=labTmp;
+}
+|
+id_
+{
+int tmpId;
+ struct lab * labTmp;
+ AvlTree tmp;
+ tmpId=getId($1,idLabList);
+
+ if (tmpId==-1)
+ {
+ idLabList=insertStringElem($1,getFreshId(),idLabList);
+ tmpId= getId($1,idLabList);
+ labTmp=makeLabel(tmpId,labTy,NULL);
+ tmp=makeAvlNode(tmpId,$1,LABEL);
+ tmp->data.labPtr=labTmp;
+ syst->idDic=Insert(tmp, syst->idDic);
+ }
+ else
+ labTmp=makeLabel(tmpId,labTy,NULL);
+ $$=labTmp;
+}
+;
+
+elastic_locations :
+elastic_location elastic_locations
+{
+ $1->next=$2;
+ $$=$1;
+}
+|
+elastic_location
+{
+ $$=$1;
+}
+;
+
+elastic_location :
+LOC_ id_ ':' elastic_transitions
+{
+ int tmpId;
+ AvlTree tmpavl;
+ tmpId=getId($2,destList);
+
+ if (tmpId==-1)/*la location n'a pas encore été déclarée comme une destination*/
+ {
+ idLocList=insertStringElem($2,getFreshId(),idLocList);
+ tmpId=getId($2,idLocList);
+ }
+ else
+ idLocList=insertStringElem($2,tmpId,idLocList); /* déjà dans la liste des destinations mais nulle part ailleurs*/
+
+ tmpavl= makeAvlNode(tmpId,$2,LOCATION);
+ tmpavl->data.locPtr=makeLocation(tmpId,NULL,NULL,$4,NULL);
+ syst->idDic=Insert(tmpavl,syst->idDic);
+
+ $$=tmpavl->data.locPtr;
+}
+;
+
+elastic_transitions :
+elastic_transition elastic_transitions
+{
+ $1->next=$2;
+ $$=$1;
+}
+|
+{
+ $$=NULL;
+}
+;
+
+elastic_transition :
+
+WHEN_ elastic_rectangular_predicate elastic_update_var GOTO_ id_ ';'
+{
+ int tmpId;
+ tmpId=getId($5,idLocList);
+
+ if (tmpId==-1) /*la location n'a pas encore été déclarée*/
+ {
+ tmpId=getId($5,destList);
+ if (tmpId==-1)
+ {
+ destList=insertStringElem($5,getFreshId(),destList);
+ tmpId=getId($5,destList); /*on vérifiera + tard si la location existe vraiment*/
+ }
+ }
+
+ $$=makeTransition(tmpId,-1,ORDINARY,$2,$3,NULL);
+}
+|
+WHEN_ elastic_event_synchro '&' elastic_rectangular_predicate elastic_update_var GOTO_ id_ ';'
+{
+ int tmpId;
+ tmpId=getId($7,idLocList);
+
+ if (tmpId==-1)/*la location n'a pas encore été déclarée*/
+ {
+ tmpId=getId($7,destList);
+ if (tmpId==-1) /*la location n'a pas encore été employée comme destination*/
+ {
+ destList=insertStringElem($7,getFreshId(),destList);
+ tmpId=getId($7,destList); /*on vérifiera + tard si la location existe vraiment*/
+
+ }
+ }
+ $$=makeTransition(tmpId,$2,ORDINARY,$4,$5,NULL);
+}
+|
+WHEN_ elastic_event_synchro elastic_update_var GOTO_ id_ ';'
+{
+ int tmpId;
+ tmpId=getId($5,idLocList);
+
+ if (tmpId==-1)/*la location n'a pas encore été déclarée*/
+ {
+ tmpId=getId($5,destList);
+ if (tmpId==-1)
+ {
+ destList=insertStringElem($5,getFreshId(),destList);
+ tmpId=getId($5,destList); /*on vérifiera + tard si la location existe vraiment*/
+ }
+ }
+ $$=makeTransition(tmpId,$2,ORDINARY,NULL,$3,NULL);
+}
+|
+WHEN_ elastic_rectangular_predicate elastic_order_synchro elastic_update_var GOTO_ id_ ';'
+{
+ int tmpId;
+ tmpId=getId($6,idLocList);
+
+ if (tmpId==-1)/*la location n'a pas encore été déclarée*/
+ {
+ tmpId=getId($6,destList);
+ if (tmpId==-1)
+ {
+ destList=insertStringElem($6,getFreshId(),destList);
+ tmpId=getId($6,destList); /*on vérifiera + tard si la location existe vraiment*/
+ }
+ }
+ $$=makeTransition(tmpId,$3,ORDINARY,$2,$4,NULL);
+}
+;
+
+elastic_event_synchro :
+GET_ id_ code_lego
+{
+ int tmpId;
+ tmpId=getId($2,idLabList);
+
+ if (tmpId==-1)
+ yyerror("Use of a non declared label. \n");
+ $$=tmpId;
+}
+;
+
+code_lego :
+'#' codeLego_ '#'
+{
+
+}
+|
+{
+
+}
+;
+
+elastic_rectangular_predicate :
+elastic_rectangular_constraint '&' elastic_rectangular_predicate
+{
+ $$=makeExpr(AND,$1,$3,NULL);
+}
+|
+elastic_rectangular_constraint
+{
+ $$=$1;
+}
+;
+
+elastic_rectangular_constraint :
+id_ op pos_rational_addition
+{
+ int tmpId;
+ AvlTree tmp;
+ tmpId=getId($1,idVarList);
+ if (tmpId==-1)
+ yyerror("Use of a non declared variable. \n");
+ tmp = Find(tmpId,syst->idDic);
+ if (tmp->data.vType!=DISCRETE && $2==EQU)
+ yyerror("Equality test is only allowed on discrete variable in Elastic. \n");
+
+ $$=makeExpr($2,
+ makeExpr(TERM,
+ NULL,
+ NULL,
+ makeTerm(tmpId,makeRational(POSITIVE,1,1),NORMAL)
+ ),
+ $3,
+ NULL);
+}
+|
+pos_rational_addition op id_
+{
+ int tmpId;
+ int op;
+ tmpId=getId($3,idVarList);
+
+ if (tmpId==-1)
+ yyerror("Use of a non declared variable. \n");
+ switch($2)
+ {
+ case GEQ :
+ op=LEQ;
+ break;
+ case LEQ :
+ op=GEQ;
+ break;
+ default :
+ break;
+ }
+ /*the elastic expression are always parsed in the same sense : id on the left, linear expression on the right*/
+ $$=makeExpr(op,makeExpr(TERM,NULL,NULL,makeTerm(tmpId,makeRational(POSITIVE,1,1),NORMAL)),$1,NULL);
+}
+|
+TRUE_
+{
+ $$=makeExpr(TRUE,NULL,NULL,NULL);
+}
+;
+
+op :
+EQU_
+{
+ $$=EQU;
+}
+|
+LEQ_
+{
+ $$=LEQ;
+}
+|
+GEQ_
+{
+ $$=GEQ;
+}
+;
+
+pos_rational_addition :
+pos_rational_addition '+' pos_rational
+{
+ $$=makeExpr(PLUS,$1,makeExpr(TERM,NULL,NULL,makeTerm(-1,$3,CONSTANT)),NULL);
+}
+|
+pos_rational
+{
+ $$=makeExpr(TERM,NULL,NULL,makeTerm(-1,$1,CONSTANT));
+}
+;
+
+pos_rational :
+positive_integer_
+{
+ $$=makeRational(POSITIVE, $1,1);
+}
+|
+positive_integer_ '/' positive_integer_
+{
+ $$=makeRational(POSITIVE, $1,$3);
+ /*printf("numérateur : %i , dénominateur : %i \n",$1,$3);*/
+}
+;
+
+elastic_order_synchro :
+PUT_ id_ code_lego
+{
+ int tmpId;
+ tmpId=getId($2,idLabList);
+
+ if (tmpId==-1)
+ yyerror("Use of a non declared label. \n");
+ $$=tmpId;
+}
+;
+
+elastic_update_var :
+DO_ '{' elastic_update_list '}'
+{
+ $$=$3;
+}
+|
+{
+ $$=NULL;
+}
+;
+