Skip to content

T
tiamo
Commit 3b114ae3 authored by Maximilien Colange's avatar Maximilien Colange
Browse files
Options

Remove old parsing files.

parent 2f503afc
Expand all Hide whitespace changes
Inline Side-by-side
Showing with 61 additions and 1037 deletions
src/timedAutomaton.ml
View file @ 3b114ae3
......@@ -10,6 +10,7 @@ sig
type timed_automaton
type discrete_state
type transition
type edge
module DS : Hashtbl.HashedType with type t = discrete_state
......
src/uta.ml 0 → 100644
View file @ 3b114ae3
open Printf
exception Var_already_defined
exception Var_undefined of string
module VarContext =
struct
type 'a t = {
index2var : (int,'a) Hashtbl.t;
var2index : ('a,int) Hashtbl.t;
mutable nextVarIndex : int;
}
let create () =
{
var2index = Hashtbl.create 10;
index2var = Hashtbl.create 10;
nextVarIndex = 0;
}
let get_var2index vc =
vc.var2index
let index_of_var vc var =
Hashtbl.find vc.var2index var
let var_of_index vc index =
try
Hashtbl.find vc.index2var index
with
| Not_found ->
eprintf "No var with index %d\n Size: %d\n" index (Hashtbl.length vc.index2var);
Hashtbl.iter (fun index var ->
eprintf "CLOCK: %d %s\n" index var) vc.index2var;
flush stderr;
raise Not_found
| _ as e -> raise e
let index2var = var_of_index
let var2index = index_of_var
let mem vc var =
Hashtbl.mem vc.var2index var
let add vc ?id var =
if ( mem vc var ) then
raise (Var_already_defined );
match id with
None ->
let index = vc.nextVarIndex in
vc.nextVarIndex <- vc.nextVarIndex + 1;
Hashtbl.add vc.index2var index var;
Hashtbl.add vc.var2index var index
| Some id ->
Hashtbl.add vc.index2var id var;
Hashtbl.add vc.var2index var id
let size vc =
Hashtbl.length vc.index2var
let iter f vc =
Hashtbl.iter f vc.var2index
end
uppaal_parser/_tags deleted 100644 → 0
View file @ 2f503afc
<*>: bin_annot, package(batteries), package(str), package(xml-light), debug, custom
uppaal_parser/uta.ml deleted 100644 → 0
View file @ 2f503afc
This diff is collapsed.
uppaal_parser/utaLexer.mll deleted 100644 → 0
View file @ 2f503afc
(* Simplify with this:
http://plus.kaist.ac.kr/~shoh/ocaml/ocamllex-ocamlyacc/ocamllex-tutorial/sec-toy-language.html
*)
{
open UtaParser
open Printf
let incr_linenum lexbuf =
let pos = lexbuf.Lexing.lex_curr_p in
lexbuf.Lexing.lex_curr_p <- { pos with
Lexing.pos_lnum = pos.Lexing.pos_lnum + 1;
Lexing.pos_bol = pos.Lexing.pos_cnum;
}
;;
}
let digit = ['0'-'9']+
let id = ['a'-'z' '_' 'A'-'Z'] ['a'-'z' 'A'-'Z' '_' '0'-'9']*
rule token = parse
| digit as inum
{NUM(int_of_string inum)}
| [' ' '\t'] { token lexbuf }
| "\n" { incr_linenum lexbuf; token lexbuf}
| "/*" {longcomment_lang lexbuf}
| "//" {onelinecomment_lang lexbuf}
| "<=" | "&lt;=" {LEQ}
| "<" | "&lt;" {LE}
| ">=" | "&gt;=" {GEQ}
| ">" | "&gt;" {GE}
| "==" {EQ}
| "=" {ASSIGN}
| "[" {LSBRACK}
| "]" {RSBRACK}
| ":=" {ASSIGN}
| "&amp;" | "&" {AMPERSAND}
| "&amp;&amp;" | "&&" | "and" {AND}
| "or" {OR}
| "not" {NOT}
| "\n" | "\t" {token lexbuf}
| "E<>" {RQUERY}
| "+" {PLUS}
| "-" {MINUS}
| "*" {MULT}
| "/" {DIV}
| "(" {LPAR}
| ")" {RPAR}
| "true" {NUM(1)}
| "false" {NUM(0)}
| "bool" {BOOL}
| "clock" {CLOCK}
| "chan" {CHAN}
| "int" {INT}
| "const" {CONST}
| "urgent" {URGENT}
| ";" {SCOLON}
| "," {COMMA}
| "system" {SYSTEM}
| "." {DOT}
| id as text {ID(text)}
| _ as t {fprintf stderr "Line %d : Unknown token : %c\n"
(lexbuf.Lexing.lex_curr_p.Lexing.pos_lnum)t; raise (Failure "Unknown token")}
| eof {EOF}
and longcomment_lang = parse
| "*/" {token lexbuf}
| "\n" { incr_linenum lexbuf; longcomment_lang lexbuf}
| _ {longcomment_lang lexbuf}
and onelinecomment_lang = parse
| "\n" { incr_linenum lexbuf; token lexbuf}
| eof {EOF}
| _ {onelinecomment_lang lexbuf}
uppaal_parser/utaParser.mly deleted 100644 → 0
View file @ 2f503afc
%{
open Printf
open Uta
%}
%token <int> NUM
%token <string> ID
%token SYSTEM CONST URGENT
%token LE LEQ GE GEQ EQ AND OR EOF
%token PLUS MINUS MULT DIV
%token CLOCK CHAN INT
%token SCOLON COMMA ASSIGN
%token LPAR RPAR LSBRACK RSBRACK
%token RQUERY NOT DOT
%token TRUE FALSE BOOL
%token AMPERSAND
%left PLUS MINUS
%left MULT DIV
%left OR
%left AND
%nonassoc UMINUS
%type <Uta.parameter list> template_parameter_list
%type <Uta.temp_declaration> declaration
%type <Uta.guard> guard
%type <Uta.update> updates
%type <(string * string * (Uta.paramArg list)) list> system
%type <Uta.query> query
%start template_parameter_list
%start guard
%start query
%start declaration
%start updates
%start system
%%
template_parameter:
CONST INT ID {ParamInt $3}
| INT AMPERSAND ID {ParamVarRef $3}
| CLOCK AMPERSAND ID {ParamClockRef $3}
template_parameter_list:
{[]}
| template_parameter {[$1]}
| template_parameter COMMA template_parameter_list {$1 :: $3}
id_list : ID SCOLON {[$1]}
| ID COMMA id_list {$1 :: $3 }
id_assign_list : ID ASSIGN NUM SCOLON {[($1,$3)]}
| ID ASSIGN NUM COMMA id_assign_list
{($1,$3) :: $5}
clock_declaration:
CLOCK id_list {$2}
expression:
NUM {Constant($1)}
| ID {Variable($1)}
| expression PLUS expression {Sum($1,$3)}
| expression MINUS expression {Subtraction($1,$3)}
| expression MULT expression {Product($1,$3)}
| expression DIV expression {Division($1,$3)}
| MINUS expression %prec UMINUS {Subtraction(Constant(0),$2)}
| LPAR expression RPAR {$2}
int_range:
{}|
LSBRACK expression COMMA expression RSBRACK {}
int_declaration:
INT int_range id_assign_list {List.map (fun x -> Var(x)) $3}
| INT int_range id_list
{
List.map (fun x -> Var(x,0)) $3
}
| BOOL id_list
{
List.map (fun x -> Var(x,0)) $2
}
const_int_declaration:
CONST INT id_assign_list
{List.map (fun x -> ConstVar(x)) $3}
chan_declaration:
CHAN id_list {$2}|
URGENT CHAN id_list {
eprintf "Parse warning: urgent channels are not supported, assuming regular channel\n";
$3
}
atomic_guard:
expression LE expression {GuardLess($1,$3)}
| expression LEQ expression {GuardLeq($1,$3)}
| expression GE expression {GuardGreater($1,$3)}
| expression GEQ expression {GuardGeq($1,$3)}
| expression EQ expression {GuardEqual($1,$3)}
| ID {GuardGreater(Variable($1),Constant(0))}
guard:
atomic_guard {[$1]}
| atomic_guard AND guard {$1 :: $3}
| atomic_guard COMMA guard {$1 :: $3}
atomic_update: ID ASSIGN expression {($1,$3)}
updates:
atomic_update {[$1]} | atomic_update COMMA updates {$1 :: $3}
declaration:
{[],[],[]}
| clock_declaration declaration
{
let clocks, ints, chans = $2 in
($1 @ clocks), ints, chans
}
| int_declaration declaration
{
let clocks, ints, chans = $2 in
clocks, ($1 @ ints), chans
}
| chan_declaration declaration
{
let clocks, ints, chans = $2 in
clocks, ints, ($1 @ chans)
}
| const_int_declaration declaration
{
let clocks, ints, chans = $2 in
clocks, ($1 @ ints), chans
}
param_arg:
NUM {Num $1}
| ID {Id $1}
arg_list:
{[]} | param_arg {[$1]} | param_arg COMMA arg_list { $1 :: $3 }
process_decl:
{[]}| ID ASSIGN ID LPAR arg_list RPAR SCOLON process_decl {($1,$3,$5) :: $8}
system: process_decl SYSTEM id_list
{
let proctypes = $1 in
let get_type proc =
let rec aux = function
| [] -> proc,proc,[]
| (p,t,s) :: _ when p = proc -> proc,t,s
| (p,_,_) :: l -> aux l
in
aux proctypes
in
List.map (fun p -> get_type p) $3
}
boolean_query:
ID DOT ID {AtomicQuery($1^"."^$3)}
| NOT ID DOT ID {NotQuery(AtomicQuery($2^"."^$4))}
| boolean_query AND boolean_query
{AndQuery($1,$3)}
| boolean_query OR boolean_query
{OrQuery($1,$3)}
| NOT LPAR boolean_query RPAR
{NotQuery($3)}
| LPAR boolean_query RPAR
{$2}
query: RQUERY boolean_query {ReachQuery($2)}
%%
uppaal_parser/utaReader.ml deleted 100755 → 0
View file @ 2f503afc
This diff is collapsed.
Markdown is supported
0% or
You are about to add 0 people to the discussion. Proceed with caution.
Finish editing this message first!
Please register or to comment