Commit e309d144 authored by Maximilien Colange's avatar Maximilien Colange

Merge branch 'master' into packaging

parents 8e75b8d0 1bc7cdf2
SUBDIRS = utap
INCLUDEDIR=@UDBML_ROOT@/udbml
UPPAAL_DIR=@UDBML_ROOT@/uppaal/lib
BUILDDIR=_build
OCAMLBUILD=ocamlbuild -use-ocamlfind -classic-display -build-dir $(BUILDDIR) @OCAMLBUILDFLAGS@
OCAMLBUILD=OCAMLPATH=@UDBML_ROOT@ ocamlbuild -use-ocamlfind -classic-display -build-dir $(BUILDDIR) @OCAMLBUILDFLAGS@
UTAP_INCLUDEDIR=@abs_top_srcdir@/utap/src
UTAP_LIB=@abs_top_srcdir@/utap/src/libutap.a
CXX_FLAGS=-std=c++11 @TIAMO_MACROS@ -I$(UTAP_INCLUDEDIR) -I@abs_top_srcdir@/src
XML_LINK_FLAGS=$(foreach i,$(XML_LIBS),-cclib $i)
CXX_FLAGS=-std=c++11 -I$(UTAP_INCLUDEDIR) -I@abs_top_srcdir@/src
SUFFIXES = .native .ml
all-local: tiamo
tiamo: src/main.native
cp `readlink -f $(BUILDDIR)/$<` tiamo
cp $(BUILDDIR)/$< tiamo
src/main.native: src/ctime.o
src/main.native: src/timedAutomatonBuilder.o
.ml.native:
CXX_FLAGS="$(CXX_FLAGS)" $(OCAMLBUILD) -cflags "-I $(INCLUDEDIR)" -lflags "$(INCLUDEDIR)/udbml.cmxa $(UTAP_LIB) $(XML_LINK_FLAGS) -cclib -L$(INCLUDEDIR)" $@
rm -f $(BUILDDIR)/$@
XML_LINK_FLAGS="$(XML_LIBS)" CXX_FLAGS="$(CXX_FLAGS)" $(OCAMLBUILD) -pkg udbml -lflags "-cclib -L$(UPPAAL_DIR) -cclib -ludbm" $@
.c.o:
CXX_FLAGS="$(CXX_FLAGS)" $(OCAMLBUILD) -pkg udbml $@
clean-local:
$(OCAMLBUILD) -clean
rm -f tiamo
# test part
TEST_EXTENSIONS = .data
DATA_LOG_DRIVER = ./teamcity-test-driver
DATA_LOG_COMPILER = ./run_test.pl
TESTS = \
tests/test_1.data \
tests/test_2.data \
tests/test_3.data \
tests/test_4.data \
tests/test_5.data \
tests/test_6.data \
tests/test_7.data \
tests/test_8.data \
tests/test_9.data \
tests/test_10.data \
tests/test_11.data \
tests/test_12.data \
tests/test_13.data \
tests/test_14.data \
tests/test_15.data \
tests/test_16.data \
tests/test_17.data \
tests/test_18.data
......@@ -14,12 +14,6 @@ if test "x${with_udbml}" != x; then
AC_SUBST([UDBML_ROOT],[${with_udbml}])
fi
dnl Check for CORA extensions
AC_ARG_ENABLE(cora,
AS_HELP_STRING([--enable-cora], [enable UPPAAL CORA extensions]),
AC_SUBST([TIAMO_MACROS],["-DENABLE_CORA"])
)
dnl Check for libxml2
AC_ARG_WITH(libxml2-prefix,
[ --with-libxml2-prefix=[=DIR] set prefix for libxml2 installation],
......
......@@ -28,17 +28,9 @@ let ocaml_cxx_flags = fun flags ->
let camlflags = List.flatten (List.map (fun opt -> ["-ccopt"; opt]) flags) in
atomize camlflags
(* TODO add C options when seeing tags:
* noassert -> add '-DNDEBUG'
*
* This kind of tags (debug, noassert, optimization levels...) should be set
* by the configure script through the _tags.in file.
*)
let _ =
dispatch begin function
| After_rules ->
(* TODO declare the internal utap library here *)
(* a custom noassert flag, only for compilation, not preprocessing *)
flag ["compile";"noassert"] (A"-noassert");
......@@ -48,8 +40,23 @@ let _ =
flag ["c++";"debug"] (ocaml_cxx_flags ["-g"]);
flag ["c++";"noassert"] (ocaml_cxx_flags ["-DNDEBUG"]);
(* explicit link dependency for C-based object files *)
pdep ["link"] "linkdep" (fun param -> [param])
(* hard-coding the C file and utap library seems the easiest way
* to avoid problems in object ordering at link time.
* Unfortunately, the dependency is not handled through ocamlbuild,
* but in the Makefile directly.
*)
let xml_flags =
try
Sys.getenv "XML_LINK_FLAGS"
with Not_found -> "-lxml2"
in
flag ["ocaml"; "link"; "native"]
(S[ P"src/ctime.o";
P"src/timedAutomatonBuilder.o";
A"-cclib"; A("-L"^(Pathname.pwd / "utap/src"));
A"-cclib"; A"-lutap";
A"-cclib"; A xml_flags
]);
| _ -> ()
end
......
#! /usr/bin/perl
print "Running test : $ARGV[0] \n";
open IN, "< $ARGV[0]";
my $title = <IN>;
chomp $title;
my $call = <IN>;
chomp $call;
my $nominal;
my %expected;
while (my $line = <IN>) {
chomp $line;
if ($line =~ s/Result of verification is //) {
$nominal = $line;
}
# gather stats
if ($line =~ s/^discrete states://) {
my @splitline = split(' ',$line);
$expected{"ds"} = $splitline[0];
}
if ($line =~ s/^states seen://) {
my @splitline = split(' ',$line);
$expected{"ss"} = $splitline[0];
}
if ($line =~ s/^states explored://) {
my @splitline = split(' ',$line);
$expected{"se"} = $splitline[0];
}
if ($line =~ s/^incl tests://) {
my @splitline = split(' ',$line);
$expected{"incl"} = $splitline[0];
}
if ($line =~ s/^pos\. incl tests://) {
my @splitline = split(' ',$line);
$expected{"pincl"} = $splitline[0];
}
}
close IN;
# Now run the tool#
# print "syscalling : $call \n";
print "##teamcity[testStarted name='$title']\n";
my $tested;
my @outputs = ();
my @results = `$call 2>&1;`;
while (my $line = shift(@results)) {
chomp $line;
push (@outputs,$line);
if ($line =~ s/Result of verification is //) {
$tested = $line;
}
# report some stats to teamcity
if ($line =~ s/^discrete states://) {
my @splitline = split(' ',$line);
my $exp = $expected{"ds"};
if ($splitline[0] != $exp) {
print "##teamcity[message text='number of discrete states $splitline[0] differs from nominal $exp' status='WARNING']\n";
}
}
if ($line =~ s/^states seen://) {
my @splitline = split(' ',$line);
my $exp = $expected{"ss"};
if ($splitline[0] != $exp) {
print "##teamcity[message text='number of states seen $splitline[0] differs from nominal $exp' status='WARNING']\n";
}
}
if ($line =~ s/^states explored://) {
my @splitline = split(' ',$line);
my $exp = $expected{"se"};
if ($splitline[0] != $exp) {
print "##teamcity[message text='number of states explored $splitline[0] differs from nominal $exp' status='WARNING']\n";
}
}
if ($line =~ s/^incl tests://) {
my @splitline = split(' ',$line);
my $exp = $expected{"incl"};
if ($splitline[0] != $exp) {
print "##teamcity[message text='number of inclusion tests $splitline[0] differs from nominal $exp' status='WARNING']\n";
}
}
if ($line =~ s/^pos\. incl tests://) {
my @splitline = split(' ',$line);
my $exp = $expected{"pincl"};
if ($splitline[0] != $exp) {
print "##teamcity[message text='number of successful inclusiontests $splitline[0] differs from nominal $exp' status='WARNING']\n";
}
}
}
# retrieve the exit value of the test
my $failure;
if ($? == 0) {
$failure = 0;
} else {
$failure = 1;
}
my $tc_output = join("|n", @outputs);
# escape characters for TeamCity
$tc_output =~ s/\[/\|\[/g;
$tc_output =~ s/\]/\|\]/g;
$tc_output =~ s/'/\|'/g;
my $reg_output = join("\n", @outputs);
if ( $failure ) {
print "$reg_output\n";
print "\n##teamcity[testFailed name='$title' message='test did not exit properly' details='$tc_output' expected='$nominal' actual='$tested'] \n";
print "Expected : $nominal Obtained : $tested \n";
my $exitval = $? >> 8;
print "test exited with value $exitval\n";
} elsif ( $nominal ne $tested ) {
print "$reg_output\n";
print "\n##teamcity[testFailed name='$title' message='regression detected' details='$tc_output' expected='$nominal' actual='$tested'] \n";
print "Expected : $nominal Obtained : $tested \n";
} else {
# print "##teamcity[buildStatisticValue key='testDuration' value='@tested[2]']\n";
# print "##teamcity[buildStatisticValue key='testMemory' value='@tested[3]']\n";
print "Test successful : $title \n";
print "Control Values/Obtained : \n$title\n$nominal\n$tested\n";
}
print "##teamcity[testFinished name='$title']\n";
<*>: bin_annot
<*.c> or <*.cm{o,x}> or <main.native>: custom @OCAMLTAGS@
<main.native>: use_dynlink, linkdep(src/timedAutomatonBuilder.o)
<costs.ml>: pp(camlp4o pa_macro.cmo @TIAMO_MACROS@)
<timedAutomatonBuilder.c>: c++
<main.native>: use_dynlink
<timedAutomatonBuilder.c> or <ctime.c>: c++
open Expression
IFDEF ENABLE_CORA THEN
let enable_cora = ref false
type edge_cost = expression
type loc_rate = expression option
type edge_cost = expression
type loc_rate = expression option
let edge_cost_def = Constant(0)
let loc_rate_def = None
let edge_cost_def = Constant(0)
let loc_rate_def = None
let get_rate rates eval_exp =
let get_rate rates eval_exp =
if !enable_cora then
Array.fold_left (fun c -> function
| None -> c
| Some(e) -> c + eval_exp e) 0 rates
ELSE
type edge_cost = unit
type loc_rate = unit
let edge_cost_def = ()
let loc_rate_def = ()
let get_rate _ _ = 1
END
else
1
extern "C" {
#include <caml/mlvalues.h>
#include <caml/memory.h>
#include <caml/callback.h>
}
#include <chrono>
extern "C" CAMLprim value
time_measure_function(value f)
{
CAMLparam1(f);
CAMLlocal1(res);
std::chrono::time_point<std::chrono::system_clock> start, end;
start = std::chrono::system_clock::now();
res = caml_callback(f, Val_unit);
end = std::chrono::system_clock::now();
std::chrono::seconds elapsed_seconds = std::chrono::duration_cast<std::chrono::seconds>(end-start);
CAMLreturn(caml_callback2(*caml_named_value("cb_build_pair"), Val_long(elapsed_seconds.count()), res));
}
......@@ -17,11 +17,11 @@ type guard_t = atomic_guard list
(* a printer for an atomic guard *)
let print_ag clocks = function
| LT(c,k) -> (VarContext.var_of_index clocks c) ^ " < " ^ (string_of_int k)
| LEQ(c,k) -> (VarContext.var_of_index clocks c) ^ " <= " ^ (string_of_int k)
| GT(c,k) -> (VarContext.var_of_index clocks c) ^ " > " ^ (string_of_int k)
| GEQ(c,k) -> (VarContext.var_of_index clocks c) ^ " <= " ^ (string_of_int k)
| EQ(c,k) -> (VarContext.var_of_index clocks c) ^ " == " ^ (string_of_int k)
| LT(c,k) -> (clocks c) ^ " < " ^ (string_of_int k)
| LEQ(c,k) -> (clocks c) ^ " <= " ^ (string_of_int k)
| GT(c,k) -> (clocks c) ^ " > " ^ (string_of_int k)
| GEQ(c,k) -> (clocks c) ^ " <= " ^ (string_of_int k)
| EQ(c,k) -> (clocks c) ^ " == " ^ (string_of_int k)
(* a printer for a guard *)
let rec print_guard clocks = function
......@@ -38,8 +38,8 @@ type reset_t = Common.clock_t * int
(* a printer for a list of resets *)
let rec print_resets clocks = function
| [] -> " "
| [(c,k)] -> VarContext.var_of_index clocks c ^ " := " ^ (string_of_int k)
| (c,k) :: l -> VarContext.var_of_index clocks c ^ " := " ^ (string_of_int k) ^ (print_resets clocks l)
| [(c,k)] -> clocks c ^ " := " ^ (string_of_int k)
| (c,k) :: l -> clocks c ^ " := " ^ (string_of_int k) ^ (print_resets clocks l)
(**
* The interface of Timed Automaton to implement when you want to provide
......@@ -50,8 +50,15 @@ sig
type ta
type state
(* retrieves ALL the clocks of the model *)
val clocks : ta -> VarContext.t
(* the number of clocks *)
(**
* WARNING: clocks are numbered from 1 to nb_clocks
* the clock of index 0 (reference clock) is implicit.
* DO NOT account for clock 0 in nb_clocks.
*)
val nb_clocks : ta -> int
(* clock names *)
val string_of_clock : ta -> int -> string
(* the initial state *)
val initial_state : ta -> state
......
(**
* an atomic guard is a tuple (c,k,r), where c is a clock id (see VarContext)
* and k is a constant and r is one of <, <=, >, >= or ==.
* Diagonal guards are not allowed.
*)
type atomic_guard =
LT of int * int
| LEQ of int * int
| GT of int * int
| GEQ of int * int
| EQ of int * int
(* a guard is a conjunction of atomic guards *)
type guard_t = atomic_guard list
(**
* a reset is a pair (c,k), where c is a clock id (see VarContext)
* and k is a constant.
*)
type reset_t = Common.clock_t * int
(** Printing functions *)
(* they are provided to help you pretty-print your custom automaton *)
(* Those functions need to know the clock names, so the first argument
* you must provide is a function that associates a name to a clock index
* Typical usage:
* let print_timed_automaton channel ta =
* ...print locations and stuff...
* Printf.printf "%s" (print_guard (string_of_clock ta) my_fancy_guard);
* ...print other stuff...
* Printf.printf "%s" (print_resets (string_of_clock ta) my_fancy_resets);
* ...print more stuff...
*)
(* a printer for an atomic guard *)
val print_ag : (int -> string) -> atomic_guard -> string
(* a printer for a guard *)
val print_guard : (int -> string) -> guard_t -> string
(* a printer for a list of resets *)
val print_resets : (int -> string) -> reset_t list -> string
(**
* The interface of Timed Automaton to implement when you want to provide
* your model as a compiled OCaml object.
*)
module type TA =
sig
type ta
type state
(* the number of clocks *)
(**
* WARNING: clocks are numbered from 1 to nb_clocks
* the clock of index 0 (reference clock) is implicit.
* DO NOT account for clock 0 in nb_clocks.
*)
val nb_clocks : ta -> int
(* clock names *)
val string_of_clock : ta -> int -> string
(* the initial state *)
val initial_state : ta -> state
(* utility functions about states *)
val hash_state : state -> int
val equal_state : state -> state -> bool
(* encodes the query on the model *)
val is_target : ta -> state -> bool
(* priority_compare s1 s2 is true iff s1 should be explored before s2 *)
(* this allows the modeller to provide heuristics about the exploration of
* the state space *)
val priority_compare : state -> state -> int
(* the transitions out of a state *)
val transitions_from : ta -> state -> (state * guard_t * (reset_t list) * state) list
(* the invariant of a state *)
val invariant : ta -> state -> guard_t
(* whether time can elapse in the state *)
val is_urgent_or_committed : ta -> state -> bool
(* the rate of a state *)
val rate_of_state : ta -> state -> int
(* the LU bounds (per clock) of a state *)
(**
* NB: larger bounds do not impact correctness.
* When in doubt, pick too large bounds.
* Remember that tight bounds yield better performance.
*)
val lubounds : ta -> state -> int array * int array
(* the global M bounds (per clock) of an automaton *)
(* this required if you want to bound the automaton *)
val global_mbounds : ta -> int array
(* to load a TA from a file *)
val model : ta
(** PRINT FUNCTIONS **)
val string_of_state : ta -> state -> string
val print_timed_automaton : out_channel -> ta -> unit
end
(**
* If you want to load a compiled module, you must implement the TA
* interface above, and you should set this variable.
* E.g.
* module MyTA : TA = struct ... end
* let _ = Ita.loadedmodule := Some (module MyTA)
*
* It is the only way provided by the Ocaml Dynlink module to access the
* dynamically loaded data.
*)
val loadedmodule : (module TA) option ref
......@@ -96,7 +96,8 @@ struct
(Pwo : PARTIAL_WO)
= Pwo(TA.DS)(TA.MDbm)(COMP)(Best(TA)(COMP))
let bestcompare = ref (module BestCost : BEST)
let walk_order = ref (module Waiting.Walk_BFS : PARTIAL_WO)
let bestcompare = ref (module HighPrio : BEST)
type res_t = M.res_t
......@@ -138,10 +139,27 @@ struct
Arg.Unit (function () -> print_path := true),
" Print a witness path (not activated by default)");
( "-mbounded",
Arg.Unit (function () -> do_bound := true),
" Use the (global M)-bounded version of the input automaton.
\tThis induces a performance hit, but guarantees termination of algorithms when you are not sure whether the input automaton is bounded or not.");
( "-cora",
Arg.Unit (function () -> Costs.enable_cora := true),
" Enable CORA-syntax support for priced models (not activated by default)");
( "-order",
Arg.String (function
| "BFS" -> walk_order := (module Waiting.Walk_BFS : PARTIAL_WO)
| "DFS" -> walk_order := (module Waiting.Walk_DFS : PARTIAL_WO)
| "BBFS" -> walk_order := (module Waiting.BBFST : PARTIAL_WO)
| "BDFS" -> walk_order := (module Waiting.BDFST : PARTIAL_WO)
| "SBFS" -> walk_order := (module Best_wait.WSTS_WO : PARTIAL_WO)
| _ -> raise (Arg.Bad "Invalid argument for option -order")),
" Sets the order in which the RG is explored:
\tBFS [default] Bread-First Search
\tDFS Depth-First Search
\tBBFS Best first (i.e. higher preference, see state variable \"preference\"), BFS on equivalent ones
\t With optimality analysis (tiamo optimal), also see -best option.
\tBDFS Best first (i.e. higher preference, see state variable \"preference\"), DFS on equivalent ones
\t With optimality analysis (tiamo optimal), also see -best option.
\tSBFS Smart BFS");
]
end
......@@ -151,7 +169,6 @@ struct
include Option_common(struct module Dbm = UDbm type res_t = bool end)
let walk_order = ref (module Waiting.Walk_BFS : PARTIAL_WO)
let abstraction = ref (module Extra_LU : ITA_ABSTRACTION)
let inclusion = ref (module Inclusion : ITA_INCLUSION)
let initial_value = ref false
......@@ -160,24 +177,13 @@ struct
let arguments = Arg.align (common_args @
[
( "-order",
Arg.String (function
| "DFS" -> walk_order := (module Waiting.Walk_DFS : PARTIAL_WO)
| "BFS" -> walk_order := (module Waiting.Walk_BFS : PARTIAL_WO)
| "SBFS" -> walk_order := (module Best_wait.WSTS_WO : PARTIAL_WO)
| _ -> raise (Arg.Bad "Invalid argument for option -order")),
" Sets the order in which the RG is explored
\tBFS [default] Bread-First Search
\tSBFS Smart BFS
\tDFS Depth-First Search");
( "-abstr",
Arg.String (function
| "LU" -> abstraction := (module Extra_LU : ITA_ABSTRACTION)
| "M" -> raise (Arg.Bad "M abstraction is currently not implemented")
| "ID" -> abstraction := (module ID_abstraction : ITA_ABSTRACTION)
| _ -> raise (Arg.Bad "Invalid argument for option -abstr")),
" Sets the abstraction to use.
" Sets the abstraction to use:
\tLU [default] LU (per discrete state) abstraction
\tM M abstraction (unimplemented)
\tID No abstraction (use with bounded automata, otherwise
......@@ -188,7 +194,7 @@ struct
| "simple" -> inclusion := (module Inclusion : ITA_INCLUSION)
| "sri" -> inclusion := (module Sri : ITA_INCLUSION)
| _ -> raise (Arg.Bad "Invalid argument for option -incl")),
" Sets the inclusion to use
" Sets the inclusion to use:
\tsimple [default] regular set inclusion
\tsri abstract inclusion (Z subset of abs_LU(Z'))");
......@@ -201,7 +207,6 @@ struct
include Option_common(struct module Dbm = PDbm type res_t = int end)
let walk_order = ref (module Waiting.Walk_BFS : PARTIAL_WO)
let abstraction = ref (module ID_abstraction : ITA_ABSTRACTION)
let inclusion = ref (module Inclusion : ITA_INCLUSION)
let initial_value = ref Dbm.PDbm.Dbm.infty
......@@ -210,31 +215,14 @@ struct
let arguments = Arg.align (common_args @
[
( "-order",
Arg.String (function
| "BFS" -> walk_order := (module Waiting.Walk_BFS : PARTIAL_WO)
| "DFS" -> walk_order := (module Waiting.Walk_DFS : PARTIAL_WO)
| "BBFS" -> walk_order := (module Waiting.BBFS : PARTIAL_WO)
| "BDFS" -> walk_order := (module Waiting.BDFS : PARTIAL_WO)
| "BBFST" -> walk_order := (module Waiting.BBFST : PARTIAL_WO)
| "BDFST" -> walk_order := (module Waiting.BDFST : PARTIAL_WO)
| "SBFS" -> walk_order := (module Best_wait.WSTS_WO : PARTIAL_WO)
| _ -> raise (Arg.Bad "Invalid argument for option -order")),
" Sets the order in which the RG is explored
\tBFS [default] Bread-First Search
\tDFS Depth-First Search
\tBBFS Best first (see option -best), BFS on equivalent ones
\tBDFS Best first (see option -best), DFS on equivalent ones
\tSBFS Smart BFS");
( "-best",
Arg.String (function
| "cost" -> bestcompare := (module BestCost : BEST)
| "pref" -> bestcompare := (module HighPrio : BEST)
| _ -> raise (Arg.Bad "Invalid argument for option -best")),
" Sets the way to chose the best candidate in waiting list (see 'BBSF' and 'BDFS' arguments of option -order)
\tcost [default] Choose the symbolic state with the smallest minimal cost (i.e. the most promising one cost-wise)
\tpref Choose the symbolic state with the highest priority, encoded in the variable \"preference\" of the model");
" Sets the way to chose the best candidate in waiting list (see 'BBSF' and 'BDFS' arguments of option -order):
\tpref [default] Choose the symbolic state with the highest preference, encoded in the variable \"preference\" of the model
\tcost Choose the symbolic state with the smallest minimal cost (i.e. the most promising one cost-wise)");
( "-incl",
Arg.String (function
......@@ -274,7 +262,7 @@ let ofile = ref ""
let load () =
match !inputtype with
| XML -> assert(!tafile <> ""); Ita.loadedmodule := Some (module Uppaalta.GenericUAutomaton(struct let tafile = !tafile;; let qfile = !qfile end))
| XML -> assert(!tafile <> ""); Ita.loadedmodule := Some (module Uppaalta.GenericUAutomaton(struct let tafile = !tafile;; let qfile = !qfile;; let enable_cora = !Costs.enable_cora end))
| CMXS ->
begin
assert(!ofile <> "");
......
......@@ -563,9 +563,9 @@ struct
let to_string ta (res,path) =
if (res = Dbm.PDbm.Dbm.infty) then
"not reachable..."
"Not reachable..."
else
Printf.sprintf "%d with path\n%s" res (Walker.path_to_string ta path)
Printf.sprintf "%d\nPath is\n%s" res (Walker.path_to_string ta path)
end
(**
* Executes a function and time it.
* The elapsed time is returned in seconds.
*)
external measure_function : (unit -> 'a) -> int * 'a = "time_measure_function";;
......@@ -95,6 +95,7 @@ struct
type timed_automaton =
{
t : BareTA.ta;
clocks : VarContext.t;
lu_tbl : (Udbml.Carray.t * Udbml.Carray.t) DSHashtbl.t;
m_tbl : Udbml.Carray.t DSHashtbl.t;
}
......@@ -102,7 +103,7 @@ struct
type edge (* TODO *)
(* indirection *)
let clocks ta = BareTA.clocks ta.t
let clocks ta = ta.clocks
(* indirection *)
let priority_compare = BareTA.priority_compare
(* indirection *)
......@@ -196,17 +197,27 @@ struct
out "(";
out (BareTA.string_of_state ta.t source);
out ",";
out (Ita.print_guard (clocks ta) guard);
out (Ita.print_guard (BareTA.string_of_clock ta.t) guard);
out ",";
out (Ita.print_resets (clocks ta) ulist);
out (Ita.print_resets (BareTA.string_of_clock ta.t) ulist);
out ",";
out (BareTA.string_of_state ta.t target);
out ")";
Buffer.contents buf
let model =
let ta = BareTA.model in
let clocks = VarContext.create () in
(* the reference clock *)
let i0 = VarContext.add clocks "t(0)" in
assert(i0 = 0);
for i = 1 to BareTA.nb_clocks ta do
let j = VarContext.add clocks (BareTA.string_of_clock ta i) in
assert(i = j)
done;
{
t = BareTA.model;
clocks = clocks;
lu_tbl = DSHashtbl.create 1024;
m_tbl = DSHashtbl.create 1024;
}
......
......@@ -359,11 +359,54 @@ make_query(const expression_t &query)
CAMLreturn(result);
}
// transforms an assignment 'e @= f' into 'e = e @ f'
// where @ is one of +,-,*,/
expression_t
normalize_assignment(const expression_t &update)
{
switch (update.getKind())
{
case Constants::ASSPLUS:
case Constants::ASSMINUS:
case Constants::ASSMULT:
case Constants::ASSDIV:
{
expression_t new_rhs;
Constants::kind_t op;
switch (update.getKind())
{
case Constants::ASSPLUS:
op = Constants::PLUS;
break;
case Constants::ASSMINUS:
op = Constants::MINUS;
break;
case Constants::ASSMULT:
op = Constants::MULT;
break;
case Constants::ASSDIV:
op = Constants::DIV;
break;
default: // cannot happen