Commit aeddbdb1 authored by Ocan Sankur's avatar Ocan Sankur

Fixed parser bug on atomic guard in queries

parent 1d795a44
...@@ -94,7 +94,6 @@ sig ...@@ -94,7 +94,6 @@ sig
val global_mbounds : ta -> int array val global_mbounds : ta -> int array
val guard_constants : ta -> int array array array val guard_constants : ta -> int array array array
val ocan : string
(* to load a TA from a file *) (* to load a TA from a file *)
val model : ta val model : ta
......
open Expression open Expression
open Printf
type atomic_guard = type atomic_guard =
| GuardLeq of expression * expression | GuardLeq of expression * expression
| GuardLess of expression * expression | GuardLess of expression * expression
...@@ -7,6 +8,25 @@ type atomic_guard = ...@@ -7,6 +8,25 @@ type atomic_guard =
| GuardGreater of expression * expression | GuardGreater of expression * expression
| GuardEqual of expression * expression | GuardEqual of expression * expression
| GuardNeq of expression * expression | GuardNeq of expression * expression
let string_of_exp = function
|Constant(c) -> sprintf "%d" c
|Variable(i) -> sprintf "V(%d)" i
|_ -> failwith "not implemented"
let string_of_atomic_guard =
function
| GuardLeq(v,exp) ->
sprintf "%s <= %s" (string_of_exp v)(string_of_exp exp)
| GuardLess(v,exp) ->
sprintf "%s < %s" (string_of_exp v)(string_of_exp exp)
| GuardGeq(v,exp)->
sprintf "%s >= %s" (string_of_exp v)(string_of_exp exp)
| GuardGreater(v,exp)->
sprintf "%s > %s" (string_of_exp v) (string_of_exp exp)
| GuardEqual(v,exp)->
sprintf "%s == %s" (string_of_exp v) (string_of_exp exp)
| GuardNeq(v,exp)->
sprintf "%s != %s" (string_of_exp v) (string_of_exp exp)
(** Atomic guard factory functions, to be registered as callbacks from C *) (** Atomic guard factory functions, to be registered as callbacks from C *)
(** This ensures that guards are in normal form GuardXX(Clock(_),_) *) (** This ensures that guards are in normal form GuardXX(Clock(_),_) *)
...@@ -24,20 +44,12 @@ let cb_atomic_guard_GT a = function ...@@ -24,20 +44,12 @@ let cb_atomic_guard_GT a = function
| _ as b -> GuardGreater(a,b) | _ as b -> GuardGreater(a,b)
let cb_atomic_guard_EQ a = function let cb_atomic_guard_EQ a = function
| Clock(_) | ClockArray(_,_) as b -> GuardEqual(b, a) | Clock(_) | ClockArray(_,_) as b -> GuardEqual(b, a)
| _ as b -> GuardEqual(a,b) | _ as b ->
GuardEqual(a,b)
let cb_atomic_guard_NEQ a = function let cb_atomic_guard_NEQ a = function
| Clock(_) | ClockArray(_,_) as b -> GuardNeq(b, a) | Clock(_) | ClockArray(_,_) as b -> GuardNeq(b, a)
| _ as b -> GuardNeq(a,b) | _ as b -> GuardNeq(a,b)
let _ =
Callback.register "cb_atomic_guard_LE" cb_atomic_guard_LE;
Callback.register "cb_atomic_guard_LT" cb_atomic_guard_LT;
Callback.register "cb_atomic_guard_GE" cb_atomic_guard_GE;
Callback.register "cb_atomic_guard_GT" cb_atomic_guard_GT;
Callback.register "cb_atomic_guard_EQ" cb_atomic_guard_EQ;
Callback.register "cb_atomic_guard_NEQ" cb_atomic_guard_NEQ
type query = type query =
| EmptyQuery | EmptyQuery
| QueryAnd of query*query | QueryAnd of query*query
...@@ -45,6 +57,23 @@ type query = ...@@ -45,6 +57,23 @@ type query =
| Location of int*int | Location of int*int
| Atomic of atomic_guard | Atomic of atomic_guard
let rec string_of_query = function
| EmptyQuery -> ""
| QueryAnd(q1,q2) ->
sprintf "(%s and %s)" (string_of_query q1) (string_of_query q2)
| QueryOr(q1,q2) ->
sprintf "(%s or %s)" (string_of_query q1) (string_of_query q2)
| Location(i,j) ->
sprintf "(%d.%d)" i j
| Atomic(g) ->
sprintf "(%s)" (string_of_atomic_guard g)
let cb_print_query q =
printf "Query: %s\n" (string_of_query q)
let cb_print_guard q =
printf "Guard: %s\n" (string_of_atomic_guard q)
let cb_print_expression q =
printf "Exp: %s\n" (string_of_exp q)
(* factory functions for query, to be registered as C callbacks *) (* factory functions for query, to be registered as C callbacks *)
let make_empty_query () = EmptyQuery let make_empty_query () = EmptyQuery
let make_query_location procId locId = Location(procId, locId) let make_query_location procId locId = Location(procId, locId)
...@@ -59,6 +88,19 @@ let _ = ...@@ -59,6 +88,19 @@ let _ =
Callback.register "cb_qb_make_and" make_query_and; Callback.register "cb_qb_make_and" make_query_and;
Callback.register "cb_qb_make_or" make_query_or; Callback.register "cb_qb_make_or" make_query_or;
Callback.register "cb_qb_make_atomic" make_query_atomic Callback.register "cb_qb_make_atomic" make_query_atomic
let _ =
Callback.register "cb_print_guard" cb_print_guard;
Callback.register "cb_print_query" cb_print_query;
Callback.register "cb_print_expression" cb_print_expression;
Callback.register "cb_atomic_guard_LE" cb_atomic_guard_LE;
Callback.register "cb_atomic_guard_LT" cb_atomic_guard_LT;
Callback.register "cb_atomic_guard_GE" cb_atomic_guard_GE;
Callback.register "cb_atomic_guard_GT" cb_atomic_guard_GT;
Callback.register "cb_atomic_guard_EQ" cb_atomic_guard_EQ;
Callback.register "cb_atomic_guard_NEQ" cb_atomic_guard_NEQ
(* A bunch of utilities callbacks to be used from C *) (* A bunch of utilities callbacks to be used from C *)
let _ = let _ =
......
...@@ -14,6 +14,7 @@ extern "C" { ...@@ -14,6 +14,7 @@ extern "C" {
#include <cassert> #include <cassert>
#include <fstream> #include <fstream>
#include <sstream> #include <sstream>
#include <streambuf>
#include <utap/utap.h> #include <utap/utap.h>
...@@ -101,7 +102,6 @@ make_expression(value process, const expression_t &expression) ...@@ -101,7 +102,6 @@ make_expression(value process, const expression_t &expression)
result = caml_callback2(*caml_named_value("cb_expression_clock"), result = caml_callback2(*caml_named_value("cb_expression_clock"),
process, process,
caml_copy_string(expression.getSymbol().getName().c_str())); caml_copy_string(expression.getSymbol().getName().c_str()));
} }
// it is a variable // it is a variable
else if (expression.getType().isIntegral()) else if (expression.getType().isIntegral())
...@@ -183,7 +183,6 @@ make_expression(value process, const expression_t &expression) ...@@ -183,7 +183,6 @@ make_expression(value process, const expression_t &expression)
printf("expr is %s\n", expression.toString().c_str()); printf("expr is %s\n", expression.toString().c_str());
caml_failwith("not a valid expression"); caml_failwith("not a valid expression");
} }
CAMLreturn(result); CAMLreturn(result);
} }
...@@ -263,6 +262,9 @@ make_atomic_guard(value process, const expression_t &atom_guard) ...@@ -263,6 +262,9 @@ make_atomic_guard(value process, const expression_t &atom_guard)
} }
assert(cb_pointer); assert(cb_pointer);
result = caml_callback2(*cb_pointer, sonleft, sonright); result = caml_callback2(*cb_pointer, sonleft, sonright);
// caml_callback(*caml_named_value("cb_print_guard"), result);
CAMLreturn(result); CAMLreturn(result);
} }
...@@ -318,6 +320,7 @@ make_query(const expression_t &query) ...@@ -318,6 +320,7 @@ make_query(const expression_t &query)
switch (query.getKind()) { switch (query.getKind()) {
case Constants::AND: case Constants::AND:
result = make_query(query[0]); result = make_query(query[0]);
for (int i = 1; i != query.getSize(); ++i) for (int i = 1; i != query.getSize(); ++i)
{ {
tmp = make_query(query[i]); tmp = make_query(query[i]);
...@@ -353,6 +356,9 @@ make_query(const expression_t &query) ...@@ -353,6 +356,9 @@ make_query(const expression_t &query)
default: default:
result = make_atomic_guard(Val_int(-1), query); result = make_atomic_guard(Val_int(-1), query);
result = caml_callback(*caml_named_value("cb_qb_make_atomic"), result);
// caml_callback(*caml_named_value("cb_print_query"), result);
break; break;
} }
...@@ -891,7 +897,10 @@ xta_from_xmlfile(value filename, value qfilename, value enable_cora) ...@@ -891,7 +897,10 @@ xta_from_xmlfile(value filename, value qfilename, value enable_cora)
{ {
// look into the .q file // look into the .q file
std::ifstream inqfile(String_val(qfilename)); std::ifstream inqfile(String_val(qfilename));
std::getline(inqfile, squery); /* Read whole file so that comments are ignored*/
// std::getline(inqfile, squery);
squery = std::string((std::istreambuf_iterator<char>(inqfile)),
std::istreambuf_iterator<char>());
} }
assert(squery != ""); assert(squery != "");
...@@ -906,12 +915,11 @@ xta_from_xmlfile(value filename, value qfilename, value enable_cora) ...@@ -906,12 +915,11 @@ xta_from_xmlfile(value filename, value qfilename, value enable_cora)
// build the caml TA (before parsing the query) // build the caml TA (before parsing the query)
result = caml_callback(*caml_named_value("cb_build_ta"), process_array); result = caml_callback(*caml_named_value("cb_build_ta"), process_array);
// parse the query // parse the query
QueryBuilder qb(ta); QueryBuilder qb(ta);
parseProperty(squery.c_str(), &qb); parseProperty(squery.c_str(), &qb);
const expression_t & query = qb.getResult(); const expression_t & query = qb.getResult();
assert(query.getKind() == Constants::EF); assert(query.getKind() == Constants::EF);
queryguard = make_query(query[0]); queryguard = make_query(query[0]);
// set the query // set the query
......
...@@ -716,12 +716,14 @@ struct ...@@ -716,12 +716,14 @@ struct
(* for each process *) (* for each process *)
for p=0 to (Array.length ta.procs)-1 do for p=0 to (Array.length ta.procs)-1 do
let proc = ta.procs.(p) in let proc = ta.procs.(p) in
(*printf "LU: doing process %s (%d) with %d locations\n"
proc.procName proc.procId (Array.length proc.procLocations); flush stdout;*)
(* initialization: for each location, add the expression of its invariant (* initialization: for each location, add the expression of its invariant
* and of guards of outgoing transitions * and of guards of outgoing transitions
*) *)
for l=0 to (Array.length proc.procLocations)-1 do for l=0 to (Array.length proc.procLocations)-1 do
let loc = proc.procLocations.(l) in let loc = proc.procLocations.(l) in
(*printf "\tLoc: %s (%d)\n" loc.locName loc.locId;*)
loc.compExpr <- Array.make nclocks ([],[]); loc.compExpr <- Array.make nclocks ([],[]);
let ag_handle = function let ag_handle = function
| GuardLeq(lhs,e) | GuardLeq(lhs,e)
...@@ -761,10 +763,9 @@ struct ...@@ -761,10 +763,9 @@ struct
loc.compExpr.(cl) <- lnew, unew loc.compExpr.(cl) <- lnew, unew
) )
(clocks_of ta lhs) (clocks_of ta lhs)
| _ as g -> | _ ->
failwith failwith
(Printf.sprintf "cannot compute LU bounds, guard is not in normal form: %s" "cannot compute LU bounds, guard is not in normal form"
(string_of_guard ta [g]))
in in
(* add invariant contribution *) (* add invariant contribution *)
...@@ -1136,7 +1137,10 @@ struct ...@@ -1136,7 +1137,10 @@ struct
let build_ta procs = build_ta_from_processes let build_ta procs = build_ta_from_processes
chans clockcont varcont var_init_values constcont const_values procs in chans clockcont varcont var_init_values constcont const_values procs in
Callback.register "cb_build_ta" build_ta; Callback.register "cb_build_ta" build_ta;
let ta_set_query ta newquery = { ta with query = newquery; } in let ta_set_query ta newquery =
(*printf "Query: %s\n" (string_of_query newquery); flush stdout;*)
{ ta with query = newquery; }
in
Callback.register "cb_set_query" ta_set_query; Callback.register "cb_set_query" ta_set_query;
utap_from_file tafile qfile utap_from_file tafile qfile
...@@ -1179,8 +1183,6 @@ struct ...@@ -1179,8 +1183,6 @@ struct
Array.iter (Array.iter (Array.sort compare)) abs'; Array.iter (Array.iter (Array.sort compare)) abs';
abs' abs'
let ocan = "ocan"
let from_file tafile qfile enable_cora ?scale:(scale=1) ?enlarge:(enlarge=0) () = let from_file tafile qfile enable_cora ?scale:(scale=1) ?enlarge:(enlarge=0) () =
let ta = make_ta tafile qfile enable_cora in let ta = make_ta tafile qfile enable_cora in
ta ta
......
E<> (p1.c and (p2.b and p3.c) and id == 0) /*asdas
*/
E<>a == 1
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