Merge branch 'master' into tests

Makefile.am

@@ -9,7 +9,7 @@ OCAMLBUILD=OCAMLPATH=@UDBML_ROOT@ ocamlbuild -use-ocamlfind -classic-display -bu
 
 UTAP_INCLUDEDIR=@abs_top_srcdir@/utap/src
 
-CXX_FLAGS=-std=c++11 @TIAMO_MACROS@ -I$(UTAP_INCLUDEDIR) -I@abs_top_srcdir@/src
+CXX_FLAGS=-std=c++11 -I$(UTAP_INCLUDEDIR) -I@abs_top_srcdir@/src
 
 SUFFIXES = .native .ml
 
@@ -18,6 +18,7 @@ all-local: tiamo
 tiamo: src/main.native
 	cp $(BUILDDIR)/$< tiamo
 
+src/main.native: src/ctime.o
 src/main.native: src/timedAutomatonBuilder.o
 
 .ml.native:

configure.ac

@@ -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],

myocamlbuild.ml

@@ -41,20 +41,21 @@ let _ =
         flag ["c++";"noassert"] (ocaml_cxx_flags ["-DNDEBUG"]);
 
         (* 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.
-	       *)
+         * 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/timedAutomatonBuilder.o";
-              A"-cclib"; A("-L"^(Pathname.pwd / "utap/src"));
-              A"-cclib"; A"-lutap";
-              A"-cclib"; A xml_flags
+        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
           ]);
 
     | _ -> ()

src/_tags.in

 <*>: bin_annot
 <*.c> or <*.cm{o,x}> or <main.native>: custom @OCAMLTAGS@
 <main.native>: use_dynlink
-<costs.ml>: pp(camlp4o pa_macro.cmo @TIAMO_MACROS@)
-<timedAutomatonBuilder.c>: c++
+<timedAutomatonBuilder.c> or <ctime.c>: c++

src/costs.ml

 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
 

src/ctime.c

+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));
+}

src/options.ml

@@ -139,6 +139,10 @@ struct
         Arg.Unit (function () -> print_path := true),
         " Print a witness path (not activated by default)");
 
+      ( "-cora",
+        Arg.Unit (function () -> Costs.enable_cora := true),
+        " Enable CORA-syntax support for priced models (not activated by default)");
+
       ( "-mbounded",
         Arg.Unit (function () -> do_bound := true),
         " Use the (global M)-bounded version of the input automaton.
@@ -265,7 +269,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 <> "");

src/time.ml

+
+(**
+ * Executes a function and time it.
+ * The elapsed time is returned in seconds.
+ *)
+external measure_function : (unit -> 'a) -> int * 'a = "time_measure_function";;
+

src/timedAutomatonBuilder.c

@@ -406,7 +406,7 @@ make_update(value process, const expression_t &u)
     CAMLlocal4(result, lhs, rhs, tmp);
     // remove compound assignments (+=, -=, *=, /=)
     expression_t update = normalize_assignment(u);
-    
+
     result = caml_callback(*caml_named_value("cb_empty_list"), Val_unit);
     switch (update.getKind())
     {
@@ -801,13 +801,9 @@ TimedAutomatonBuilder::visitProcess(instance_t &process)
         // the containing process id
         args[6] = proc_id;
         // the rate of the location
-#ifdef ENABLE_CORA
         args[7] = location.costRate.empty() ?
             caml_callback(*caml_named_value("cb_make_None"), Val_unit) :
             caml_callback(*caml_named_value("cb_make_Some"), make_expression(procref, subst_params(location.costRate, process.mapping)));
-#else
-        args[7] = Val_unit;
-#endif
         // GC-friendly version of: loc_array[loc_id] = build_location()
         caml_modify(&Field(loc_array, location_ids[&location]),
                     caml_callbackN(*caml_named_value("cb_build_location"), 8, args));
@@ -837,13 +833,13 @@ TimedAutomatonBuilder::visitProcess(instance_t &process)
 #include "utap/typechecker.h"
 
 extern "C" CAMLprim value
-xta_from_xmlfile(value filename, value qfilename)
+xta_from_xmlfile(value filename, value qfilename, value enable_cora)
 {
-    CAMLparam2(filename, qfilename);
+    CAMLparam3(filename, qfilename, enable_cora);
     CAMLlocal3(process_array, queryguard, result);
 
     // parse the input with the library utap
-    UTAP::TimedAutomataSystem * ta = new UTAP::TimedAutomataSystem();
+    UTAP::TimedAutomataSystem * ta = new UTAP::TimedAutomataSystem(Bool_val(enable_cora));
     int parse_res = parseXMLFile(String_val(filename), ta, true);
     assert(parse_res == 0);
 

utap/configure.ac

@@ -66,13 +66,6 @@ no)
   ;;
 esac
 
-dnl Check for CORA extensions
-
-AC_ARG_ENABLE(cora,
-AS_HELP_STRING([--enable-cora], [enable UPPAAL CORA extensions]),
-OPT_FLAGS="${OPT_FLAGS} -DENABLE_CORA"
-)
-
 dnl Checks for libraries.
 
 dnl Checks for header files.

utap/src/system.cpp

@@ -922,14 +922,13 @@ string chan_priority_t::toString() const
     return stream.str();
 }
 
-TimedAutomataSystem::TimedAutomataSystem(): syncUsed(0)
+TimedAutomataSystem::TimedAutomataSystem(bool enable_cora): syncUsed(0)
 {
     global.frame = frame_t::createFrame();
     addVariable(&global, type_t::createPrimitive(CLOCK), "t(0)", expression_t());
     addVariable(&global, type_t::createPrimitive(INT), "preference", expression_t());
-#ifdef ENABLE_CORA
-    addVariable(&global, type_t::createPrimitive(COST), "cost", expression_t());
-#endif
+    if (enable_cora)
+        addVariable(&global, type_t::createPrimitive(COST), "cost", expression_t());
 
     hasUrgentTrans = false;
     hasPriorities = false;
@@ -1016,7 +1015,7 @@ template_t& TimedAutomataSystem::addDynamicTemplate (std::string name,frame_t pa
     templ.dynindex = dynamicTemplates.size ()-1;
     templ.isDefined = false;
     return templ;
-   
+
 }
 
 std::vector<template_t*> & TimedAutomataSystem::getDynamicTemplates () {
@@ -1027,7 +1026,7 @@ std::vector<template_t*> & TimedAutomataSystem::getDynamicTemplates () {
             dynamicTemplatesVec.push_back(&(*it));
         }
     }
-        
+
     return dynamicTemplatesVec;
 }
 
@@ -1271,7 +1270,7 @@ void TimedAutomataSystem::accept(SystemVisitor &visitor)
     }
 
 
-    
+
     for (t = dynamicTemplates.begin(); t != dynamicTemplates.end();t++)
     {
         if (visitor.visitTemplateBefore(*t))

utap/src/utap/system.h

@@ -362,12 +362,12 @@ namespace UTAP
         std::deque<edge_t> edges;                /**< Edges */
         std::vector<expression_t> dynamicEvals;
         bool isTA;
-        
+
         int addDynamicEval (expression_t t) {
             dynamicEvals.push_back (t);
             return dynamicEvals.size()-1;
         }
-        
+
         std::vector<expression_t>& getDynamicEval () {return dynamicEvals;}
 
         /** Add another location to template. */
@@ -417,7 +417,7 @@ namespace UTAP
 
         /* returns the first update on one of the given instances, at y location */
         bool getUpdate(const std::vector<instanceLine_t*>& instances, int y, update_t*& simUpdate);
-       
+
     };
 
     /**
@@ -472,7 +472,7 @@ namespace UTAP
     class TimedAutomataSystem
     {
     public:
-        TimedAutomataSystem();
+        TimedAutomataSystem(bool enable_cora=false);
         TimedAutomataSystem(const TimedAutomataSystem&);
         virtual ~TimedAutomataSystem();
 
@@ -504,7 +504,7 @@ namespace UTAP
         template_t &addTemplate(std::string, frame_t params, const bool isTA = true,
                 const std::string type = "", const std::string mode = "");
         template_t &addDynamicTemplate(std::string, frame_t params);
-        
+
         instance_t &addInstance(
                 std::string name, instance_t &instance, frame_t params,
                 const std::vector<expression_t> &arguments);
@@ -613,9 +613,9 @@ namespace UTAP
         variable_t *addVariable(
             std::list<variable_t> &variables, frame_t frame,
             type_t type, std::string);
-        
+
         std::string location;
-        
+
     public:
         void addError(position_t, std::string, std::string context="");
         void addWarning(position_t, std::string);