diff --git a/src/ita.ml b/src/ita.ml index fd39a6a8a79da772ca58ff0654ffb0f015f06118..0fd805f1bd54cf1c8c28ce6ffd9be95ab5bdd134 100644 --- a/src/ita.ml +++ b/src/ita.ml @@ -94,7 +94,6 @@ sig val global_mbounds : ta -> int array val guard_constants : ta -> int array array array - val ocan : string (* to load a TA from a file *) val model : ta diff --git a/src/querybuilder.ml b/src/querybuilder.ml index a889ee1b648e3e9a3859596aac8c2af18525838c..07bbe2b8d82e54b278f4eb2b2681d9b44c51cdb4 100644 --- a/src/querybuilder.ml +++ b/src/querybuilder.ml @@ -1,5 +1,6 @@ open Expression - +open Printf + type atomic_guard = | GuardLeq of expression * expression | GuardLess of expression * expression @@ -7,6 +8,25 @@ type atomic_guard = | GuardGreater of expression * expression | GuardEqual 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 *) (** This ensures that guards are in normal form GuardXX(Clock(_),_) *) @@ -24,20 +44,12 @@ let cb_atomic_guard_GT a = function | _ as b -> GuardGreater(a,b) let cb_atomic_guard_EQ a = function | Clock(_) | ClockArray(_,_) as b -> GuardEqual(b, a) - | _ as b -> GuardEqual(a,b) + | _ as b -> + GuardEqual(a,b) let cb_atomic_guard_NEQ a = function | Clock(_) | ClockArray(_,_) as b -> GuardNeq(b, a) | _ 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 = | EmptyQuery | QueryAnd of query*query @@ -45,6 +57,23 @@ type query = | Location of int*int | 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 *) let make_empty_query () = EmptyQuery let make_query_location procId locId = Location(procId, locId) @@ -59,6 +88,19 @@ let _ = Callback.register "cb_qb_make_and" make_query_and; Callback.register "cb_qb_make_or" make_query_or; 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 *) let _ = diff --git a/src/timedAutomatonBuilder.c b/src/timedAutomatonBuilder.c index 4521739da36bd1f5c114c0d0b30da0c7e1980346..e5064909a2aed7dc3db60150622e7680006ae0b8 100644 --- a/src/timedAutomatonBuilder.c +++ b/src/timedAutomatonBuilder.c @@ -14,6 +14,7 @@ extern "C" { #include #include #include +#include #include @@ -101,7 +102,6 @@ make_expression(value process, const expression_t &expression) result = caml_callback2(*caml_named_value("cb_expression_clock"), process, caml_copy_string(expression.getSymbol().getName().c_str())); - } // it is a variable else if (expression.getType().isIntegral()) @@ -183,7 +183,6 @@ make_expression(value process, const expression_t &expression) printf("expr is %s\n", expression.toString().c_str()); caml_failwith("not a valid expression"); } - CAMLreturn(result); } @@ -263,6 +262,9 @@ make_atomic_guard(value process, const expression_t &atom_guard) } assert(cb_pointer); result = caml_callback2(*cb_pointer, sonleft, sonright); + // caml_callback(*caml_named_value("cb_print_guard"), result); + + CAMLreturn(result); } @@ -318,6 +320,7 @@ make_query(const expression_t &query) switch (query.getKind()) { case Constants::AND: result = make_query(query[0]); + for (int i = 1; i != query.getSize(); ++i) { tmp = make_query(query[i]); @@ -353,6 +356,9 @@ make_query(const expression_t &query) default: 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; } @@ -891,7 +897,10 @@ xta_from_xmlfile(value filename, value qfilename, value enable_cora) { // look into the .q file 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(inqfile)), + std::istreambuf_iterator()); } assert(squery != ""); @@ -906,12 +915,11 @@ xta_from_xmlfile(value filename, value qfilename, value enable_cora) // build the caml TA (before parsing the query) result = caml_callback(*caml_named_value("cb_build_ta"), process_array); - // parse the query QueryBuilder qb(ta); parseProperty(squery.c_str(), &qb); const expression_t & query = qb.getResult(); - assert(query.getKind() == Constants::EF); + assert(query.getKind() == Constants::EF); queryguard = make_query(query[0]); // set the query diff --git a/src/uppaalta.ml b/src/uppaalta.ml index 44a301243f92854c5a610be51a3a103df7c5821c..da703bf8ba6d5d5bbd3ebae06091d0887de53957 100644 --- a/src/uppaalta.ml +++ b/src/uppaalta.ml @@ -716,12 +716,14 @@ struct (* for each process *) for p=0 to (Array.length ta.procs)-1 do 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 * and of guards of outgoing transitions *) for l=0 to (Array.length proc.procLocations)-1 do let loc = proc.procLocations.(l) in + (*printf "\tLoc: %s (%d)\n" loc.locName loc.locId;*) loc.compExpr <- Array.make nclocks ([],[]); let ag_handle = function | GuardLeq(lhs,e) @@ -761,10 +763,9 @@ struct loc.compExpr.(cl) <- lnew, unew ) (clocks_of ta lhs) - | _ as g -> + | _ -> failwith - (Printf.sprintf "cannot compute LU bounds, guard is not in normal form: %s" - (string_of_guard ta [g])) + "cannot compute LU bounds, guard is not in normal form" in (* add invariant contribution *) @@ -1136,7 +1137,10 @@ struct let build_ta procs = build_ta_from_processes chans clockcont varcont var_init_values constcont const_values procs in 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; utap_from_file tafile qfile @@ -1179,8 +1183,6 @@ struct Array.iter (Array.iter (Array.sort compare)) abs'; abs' - let ocan = "ocan" - let from_file tafile qfile enable_cora ?scale:(scale=1) ?enlarge:(enlarge=0) () = let ta = make_ta tafile qfile enable_cora in ta diff --git a/tests/a.q b/tests/a.q index f77258458aae1445670a3d96435bf49d5e45cd61..edfc5abe49e5eb68b078e6c2b3cc3933eada980d 100644 --- a/tests/a.q +++ b/tests/a.q @@ -1 +1,4 @@ -E<> (p1.c and (p2.b and p3.c) and id == 0) +/*asdas + +*/ +E<>a == 1