promelaparser_withexps.opp.exp 9.5 KB
Newer Older
1 2 3 4 5 6 7 8 9 10 11 12 13 14 15 16 17
%{
open Logic_ptree
open Promelaast
open Bool3


let observed_states=Hashtbl.create 1

let to_seq c =
  [{ condition = Some c; nested = [];
    min_rep = Some (PCst (IntConstant "1"));
    max_rep = Some (PCst (IntConstant "1"));
   }]
%}
%start promela
%token EOF
%token PROMELA_AND
18 19 20 21 22 23 24
%token <string> PROMELA_CALLOF
%token <string> PROMELA_CALLORRETURNOF
%token PROMELA_COLON
%token PROMELA_DIV
%token PROMELA_DOT
%token PROMELA_DOUBLE_COLON
%token PROMELA_EQ
25
%token PROMELA_FALSE
26 27
%token PROMELA_FI
%token PROMELA_FUNC
28
%token PROMELA_GE
29 30 31 32 33 34 35 36 37 38
%token PROMELA_GOTO
%token PROMELA_GT
%token PROMELA_IF
%token <string> PROMELA_INT
%token <string> PROMELA_LABEL
%token PROMELA_LBRACE
%token PROMELA_LE
%token PROMELA_LEFT_SQUARE
%token PROMELA_LPAREN
%token PROMELA_LT
39
%token PROMELA_MINUS
40 41 42 43 44 45 46 47 48 49 50 51 52 53 54
%token PROMELA_MODULO
%token PROMELA_NEQ
%token PROMELA_NEVER
%token PROMELA_NOT
%token PROMELA_OR
%token PROMELA_PLUS
%token PROMELA_RBRACE
%token <string> PROMELA_RETURNOF
%token PROMELA_RIGHT_ARROW
%token PROMELA_RIGHT_SQUARE
%token PROMELA_RPAREN
%token PROMELA_SEMICOLON
%token PROMELA_SKIP
%token PROMELA_STAR
%token PROMELA_TRUE
55 56 57 58 59
%right PROMELA_OR
%right PROMELA_AND
%nonassoc PROMELA_FALSE PROMELA_NOT PROMELA_TRUE
%right PROMELA_EQ PROMELA_GE PROMELA_GT PROMELA_LE PROMELA_LT PROMELA_NEQ
%right PROMELA_DIV PROMELA_MINUS PROMELA_MODULO PROMELA_PLUS PROMELA_STAR
60 61 62 63
%type <Promelaast.parsed_automaton> promela
%%

promela:
64
  _1 = PROMELA_NEVER _2 = PROMELA_LBRACE _3 = states _4 = PROMELA_RBRACE _5 = EOF
65 66 67 68 69 70 71 72 73 74 75 76 77 78 79 80 81 82 83 84 85 86 87 88 89 90 91 92
    {                                                                 ( 
	    let states=
	      Hashtbl.fold (fun _ st l -> 
		if st.acceptation=Undefined || st.init=Undefined then
		  begin
		    Format.print_string ("Error: the state '"^(st.name)^"' is used but never defined.\n");
		    exit 1
		  end;
		st::l
	      ) observed_states []
	    in
	    (states , _3)
	)}
| _1 = PROMELA_NEVER _2 = PROMELA_LBRACE _3 = states _4 = PROMELA_SEMICOLON _5 = PROMELA_RBRACE _6 = EOF
    {                                                 (
	    let states=
	      Hashtbl.fold (fun _ st l -> 
		if st.acceptation=Undefined || st.init=Undefined then
		  begin
                    Aorai_option.abort 
                      "Error: state %s is used bug never defined" st.name
		  end;
		st::l
	      ) observed_states []
	    in
	    (states , _3) )}

states:
93
  _1 = states _2 = PROMELA_SEMICOLON _3 = state
94 95 96 97 98
    {                                         ( _1@_3 )}
| _1 = state
    {         ( _1 )}

state:
99
  _1 = state_labels _2 = state_body
100 101 102 103 104 105 106 107 108 109 110 111 112 113 114 115 116 117 118 119 120 121 122 123 124 125 126
    {                                  (
	  let (stl,trans)=_1 in
	  let (trl,force_final)=_2 in
	    if force_final then
	      begin
		List.iter (fun s -> 
		  try 
		    (Hashtbl.find observed_states s.name).acceptation <- True
		  with
		    | Not_found -> assert false 
                (* This state has to be in the hashtable -- by construction *)
		) stl
	      end;
	    if trl=[] then
	      trans 
	    else
	      let tr_list=
		List.fold_left (fun l1 (cr,stop_st)  -> 
		  List.fold_left (fun l2 st -> 
		    {start=st;stop=stop_st;cross=Seq (to_seq cr);numt=(-1)}::l2
		  ) l1 stl
		) [] trl
	      in
	      (List.rev tr_list)@trans
	)}

state_labels:
127
  _1 = label _2 = state_labels
128 129 130 131 132 133 134 135 136
    {                             ( 
	    let (stl1,trl1)=_1 in
	    let (stl2,trl2)=_2 in
	      (stl1@stl2,trl1@trl2) 
	)}
| _1 = label
    {         ( _1 )}

label:
137
  _1 = PROMELA_LABEL _2 = PROMELA_COLON
138 139 140 141 142 143 144 145 146 147 148 149 150 151 152 153 154 155 156 157 158 159 160 161 162 163 164 165 166 167 168 169 170 171 172 173 174 175 176 177 178 179 180 181 182 183 184 185 186 187 188 189 190 191 192
    {                                      (
	  begin
            (* Step 0 : trans is the set of new transitions and old 
               is the description of the current state *)
	    let trans = ref [] in
	    (* Promela Label is a state. According to its name, 
               we will try to give him its properties (init / accept) *)
	    (* Firstly, if this state is still referenced, 
               then we get it back. Else, we make a new "empty" state *)
	    let old= 
	      try  
		Hashtbl.find observed_states _1
	      with
		| Not_found -> 
		    let s = Data_for_aorai.new_state _1 in
		    Hashtbl.add observed_states _1 s;
		    s
	    in
            (* Step 1 : setting up the acceptance status *)
	    (* Default status : Non acceptation state *)
 	    old.acceptation <- False;
	    
	    (* Accept_all state means acceptance state with a 
               reflexive transition without cross condition *)
	    (* This case is not exclusive with the following. 
               Acceptation status is set in this last. *)
	    if (String.length _1>=10) && 
              (String.compare (String.sub _1 0 10) "accept_all")=0 
            then 
	      trans:=
                {start=old;stop=old;cross=Seq (to_seq PTrue);numt=(-1)}::!trans;
	    
	    (* If the name includes accept then this state is 
               an acceptation one. *)
	    if (String.length _1>=7) && 
              (String.compare (String.sub _1 0 7) "accept_")=0 
            then
	      old.acceptation <- True;

            (* Step 2 : setting up the init status *)
	    (* If the state name ended with "_init" then 
               it is an initial state. Else, it is not. *)
	    if (String.length _1>=5) && 
              (String.compare 
                 (String.sub _1 ((String.length _1)-5) 5) "_init" ) = 0
	    then
	      old.init <- True
	    else
	      old.init <- False;
	    
	    ([old],!trans)
	  end
	)}

state_body:
193
  _1 = PROMELA_IF _2 = transitions _3 = PROMELA_FI
194 195 196 197 198 199 200 201 202
    {                                            ( (_2,false) )}
| _1 = PROMELA_SKIP
    {                ( ([],false) )}
| _1 = PROMELA_FALSE
    {                 ( ([],true) )}
| _1 = PROMELA_IF _2 = PROMELA_DOUBLE_COLON _3 = PROMELA_FALSE _4 = PROMELA_FI
    {                                                            ( ([],true) )}

transitions:
203
  _1 = transitions _2 = transition
204 205 206 207 208
    {                                 ( _1@[_2] )}
| _1 = transition
    {              ( [_1] )}

transition:
209
  _1 = PROMELA_DOUBLE_COLON _2 = guard _3 = PROMELA_RIGHT_ARROW _4 = PROMELA_GOTO _5 = PROMELA_LABEL
210 211 212 213 214 215 216 217 218 219 220 221 222 223
    {                                                       (
	  let s=
	    try
	      Hashtbl.find observed_states _5
	    with
		Not_found -> 
		  let r = Data_for_aorai.new_state _5 in
		  Hashtbl.add observed_states _5 r;
		  r
	  in
	  (_2,s)
	)}

guard:
224
  _1 = PROMELA_CALLORRETURNOF
225 226 227 228 229 230 231 232 233 234 235 236 237 238 239 240 241 242 243 244 245
    {                          ( POr(PCall (_1,None), PReturn _1) )}
| _1 = PROMELA_CALLOF
    {                         ( PCall (_1,None) )}
| _1 = PROMELA_RETURNOF
    {                           ( PReturn _1 )}
| _1 = PROMELA_TRUE
    {                ( PTrue )}
| _1 = PROMELA_FALSE
    {                 ( PFalse )}
| _1 = PROMELA_NOT _2 = guard
    {                     ( PNot _2 )}
| _1 = guard _2 = PROMELA_AND _3 = guard
    {                           ( PAnd (_1,_3) )}
| _1 = guard _2 = PROMELA_OR _3 = guard
    {                          ( POr (_1,_3) )}
| _1 = PROMELA_LPAREN _2 = guard _3 = PROMELA_RPAREN
    {                                       ( _2 )}
| _1 = logic_relation
    {                         ( _1 )}

logic_relation:
246
  _1 = arith_relation _2 = PROMELA_EQ _3 = arith_relation
247 248 249 250 251 252 253 254 255 256 257 258 259 260 261
    {                                             ( PRel(Eq, _1, _3) )}
| _1 = arith_relation _2 = PROMELA_LT _3 = arith_relation
    {                                             ( PRel(Lt, _1, _3) )}
| _1 = arith_relation _2 = PROMELA_GT _3 = arith_relation
    {                                             ( PRel(Gt, _1, _3) )}
| _1 = arith_relation _2 = PROMELA_LE _3 = arith_relation
    {                                             ( PRel(Le, _1, _3) )}
| _1 = arith_relation _2 = PROMELA_GE _3 = arith_relation
    {                                             ( PRel(Ge, _1, _3) )}
| _1 = arith_relation _2 = PROMELA_NEQ _3 = arith_relation
    {                                             ( PRel(Neq,_1, _3) )}
| _1 = arith_relation
    {                  ( PRel(Neq,_1, PCst(IntConstant "0")) )}

arith_relation:
262
  _1 = arith_relation_mul _2 = PROMELA_PLUS _3 = arith_relation
263 264 265 266 267 268 269
    {            ( PBinop(Badd, _1 , _3))}
| _1 = arith_relation_mul _2 = PROMELA_MINUS _3 = arith_relation
    {            ( PBinop(Bsub,_1,_3) )}
| _1 = arith_relation_mul
    {                      ( _1 )}

arith_relation_mul:
270
  _1 = arith_relation_mul _2 = PROMELA_DIV _3 = access_or_const
271 272 273 274 275 276 277 278 279
    {            ( PBinop(Bdiv,_1,_3) )}
| _1 = arith_relation_mul _2 = PROMELA_STAR _3 = access_or_const
    {            ( PBinop(Bmul,_1,_3) )}
| _1 = arith_relation_mul _2 = PROMELA_MODULO _3 = access_or_const
    {            ( PBinop(Bmod,_1,_3) )}
| _1 = access_or_const
    {                   ( _1 )}

access_or_const:
280
  _1 = PROMELA_INT
281 282 283 284 285 286 287 288 289
    {                      ( PCst(IntConstant _1) )}
| _1 = PROMELA_MINUS _2 = PROMELA_INT
    {            ( PUnop (Uminus, PCst (IntConstant _2)) )}
| _1 = access
    {          ( _1 )}
| _1 = PROMELA_LPAREN _2 = arith_relation _3 = PROMELA_RPAREN
    {                                                ( _2 )}

access:
290
  _1 = access _2 = PROMELA_DOT _3 = PROMELA_LABEL
291 292 293 294 295
    {                                    ( PField (_1,_3) )}
| _1 = access_array
    {                (_1)}

access_array:
296
  _1 = access_array _2 = PROMELA_LEFT_SQUARE _3 = access_or_const _4 = PROMELA_RIGHT_SQUARE
297 298 299 300 301
    {     ( PArrget(_1,_3) )}
| _1 = access_leaf
    {                   (_1)}

access_leaf:
302
  _1 = PROMELA_STAR _2 = access
303 304 305 306 307 308 309 310 311 312 313
    {                              ( PUnop(Ustar,_2) )}
| _1 = PROMELA_LABEL _2 = PROMELA_FUNC _3 = PROMELA_DOT _4 = PROMELA_LABEL
    {                                                        ( PPrm(_1,_4) )}
| _1 = PROMELA_LABEL
    {                 ( PVar _1 )}
| _1 = PROMELA_LPAREN _2 = access _3 = PROMELA_RPAREN
    {                                        ( _2 )}

%%