← Back to branch summary

~ubuntu-branches/ubuntu/intrepid/tcm/intrepid

« back to all changes in this revision

Viewing changes to src/sd/bv/adsltlformula.y

  • Committer: Bazaar Package Importer
  • Author(s): Otavio Salvador
  • Date: 2003-07-03 20:08:21 UTC
  • Revision ID: james.westby@ubuntu.com-20030703200821-se4xtqx25e5miczi
Tags: upstream-2.20
Import upstream version 2.20

Show diffs side-by-side

added added

removed removed

Lines of Context:
src/sd/bv/adsltlformula.y
 
1
%{
 
2
#include "adsltlformulaparse.h"
 
3
#include <math.h>
 
4
#include <string.h>
 
5
#include <stdio.h>
 
6
#include <stdlib.h>
 
7
 
 
8
 
 
9
 
 
10
  /* adapted from the nusmv ltl parser */
 
11
 
 
12
 
 
13
 
 
14
  /*
 
15
typedef char *CHAR_PTR;
 
16
#define YYSTYPE CHAR_PTR
 
17
#define YYDEBUG 1
 
18
  */
 
19
 
 
20
  char *ltlprop; /* the temporal property */
 
21
  char *initial; /* predicate characterising initial configuration */
 
22
  /*  char *final; */ /*predicate characterising final configuration */
 
23
  int isfinal; /* true iff FINAL is part of requirement */
 
24
 
 
25
  char *identifier[100];    /* name of var */
 
26
  int identifier_count;
 
27
 
 
28
  char *mycpy(char *text);
 
29
  char *Mymalloc(unsigned size);
 
30
  char *mystrconcat3(char *s1, char *s2, char *s3);
 
31
  char *mystrconcat2(char *s1, char *s2);
 
32
 
 
33
  extern char adsltlformulatext[];
 
34
 
 
35
  int isltl; /* if true, then formula is ltl formula*/
 
36
 
 
37
%}
 
38
 
 
39
 
 
40
/* BISON Declarations */
 
41
%token QUOTE OPEN CLOSE  NL IDENTIFIER  COLON TRUE FALSE LEQ GEQ EQ NEQ GT LT FUTURE GLOBALLY NEXT UNTIL IMPLIES EQUIV INITI FINAL AF EG AG EF
 
42
%left   OR
 
43
%left   AND
 
44
%left  NEG NOT IN    /* negation--unary minus */
 
45
%right '^'         /* exponentiation        */
 
46
 
 
47
%union  {
 
48
  char *str_ptr;
 
49
      }  
 
50
%type  <str_ptr>   input line simple_expr ident ltlexpr orexpr andexpr untilexpr atomexpr 
 
51
 
 
52
 
 
53
 
 
54
 
 
55
 
 
56
/* Grammar follows */
 
57
%%
 
58
input:  line {ltlprop=mycpy($1);}
 
59
;
 
60
 
 
61
line:  ltlexpr 
 
62
 
 
63
;
 
64
 
 
65
 
 
66
 
 
67
simple_expr:   TRUE {$$=mycpy("TRUE");}
 
68
|              FALSE {$$=mycpy("FALSE");}
 
69
|              INITI {$$=mycpy(initial);}
 
70
|              FINAL {$$=mycpy("FINAL");isfinal=1;}
 
71
|              IN OPEN ident CLOSE { $$=mystrconcat2($3,">0");}
 
72
|              ident  {$$=$1;}
 
73
;
 
74
 
 
75
 
 
76
 
 
77
ident: IDENTIFIER {
 
78
int i;
 
79
$$ = mycpy(adsltlformulalval.str_ptr);
 
80
 i=strlen($$);
 
81
 while (i){
 
82
   if ($$[i-1]==' ') $$[i-1]='_'; /* replace spaces by underscores for model checker */
 
83
   if ($$[i-1]=='-') $$[i-1]='_'; /* replace dashes by underscores for model checker */
 
84
   i--;
 
85
 }
 
86
 identifier[identifier_count]=mycpy(adsltlformulalval.str_ptr);
 
87
 identifier_count++; 
 
88
}
 
89
;
 
90
 
 
91
ltlexpr    : orexpr {$$=$1;}
 
92
           | ltlexpr IMPLIES orexpr {$$ = mystrconcat3($1," -> ",$3);} 
 
93
           | ltlexpr EQUIV orexpr {$$ = mystrconcat3($1," <-> ",$3);} 
 
94
           ;
 
95
orexpr     : andexpr   {$$ = $1;}
 
96
           | orexpr OR andexpr  {$$ = mystrconcat3($1," | ",$3);} 
 
97
           ;
 
98
andexpr    : untilexpr    {$$=$1;}
 
99
           | andexpr AND untilexpr  {$$ = mystrconcat3($1," & ",$3);}
 
100
           ;
 
101
untilexpr  : atomexpr  {$$=$1;}
 
102
           | untilexpr UNTIL atomexpr {$$ = mystrconcat3($1," U ",$3);}
 
103
           ;
 
104
atomexpr   : NOT atomexpr       {$$ = mystrconcat2("! ",$2);} 
 
105
           | NEXT atomexpr      {$$ = mystrconcat2("X ",$2);}
 
106
           | GLOBALLY atomexpr  {$$ = mystrconcat2("G ",$2);} 
 
107
           | FUTURE atomexpr    {$$ = mystrconcat2("F ",$2);}
 
108
           | EF atomexpr        {$$ = mystrconcat2("EF ",$2);isltl=0;}
 
109
           | AF atomexpr        {$$ = mystrconcat2("AF ",$2);isltl=0;}
 
110
           | AG atomexpr        {$$ = mystrconcat2("AG ",$2);isltl=0;}
 
111
           | EG atomexpr        {$$ = mystrconcat2("EG ",$2);isltl=0;}
 
112
           | OPEN ltlexpr CLOSE {$$ = mystrconcat3("(",$2,")");}
 
113
           | simple_expr        {$$ = $1;}
 
114
           ;
 
115
 
 
116
 
 
117
 
 
118
 
 
119
 
 
120
 
 
121
 
 
122
%%
 
123
char *mystrconcat2(char *s1, char *s2)
 
124
{
 
125
  char *ret;
 
126
  int len;
 
127
  len = strlen(s1);
 
128
  len += strlen(s2);
 
129
  ret = (char *)malloc(sizeof(char)*(len+1));
 
130
  strcpy(ret,s1);
 
131
  strcat(ret,s2);
 
132
  return(ret);
 
133
}
 
134
 
 
135
 
 
136
char *mystrconcat3(char *s1, char *s2, char *s3)
 
137
{
 
138
  char *ret;
 
139
  int len;
 
140
  len = strlen(s1);
 
141
  len += strlen(s2);
 
142
  len += strlen(s3);
 
143
  ret = (char*)malloc(sizeof(char)*(len+3));
 
144
  strcpy(ret,s1);
 
145
  strcat(ret," ");
 
146
  strcat(ret,s2);
 
147
  strcat(ret," ");
 
148
  strcat(ret,s3);
 
149
  return(ret);
 
150
}
 
151
         
 
152
 
 
153
char *mycpy(char *text)
 
154
{
 
155
  char *cptr;
 
156
  cptr = (char *) Mymalloc(strlen(text) + 1);
 
157
  strcpy(cptr, text);
 
158
  return(cptr);
 
159
}
 
160
 
 
161
char *Mymalloc(unsigned size)
 
162
{
 
163
  char *ret;
 
164
 
 
165
  ret = malloc(size);
 
166
  if (ret == NULL) {
 
167
    printf("malloc returns NULL\n");
 
168
    exit(1);
 
169
  }
 
170
  return(ret);
 
171
}  
 
172