Skip to content

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

Refactor VarContext for a uniform handling of arrays.

parent d2c1b049
Expand all Hide whitespace changes
Inline Side-by-side
Showing with 347 additions and 298 deletions
src/main.ml
View file @ b32d83ce
......@@ -60,7 +60,7 @@ let set_command arg =
) else anon_arguments arg
let main() =
(* Printexc.record_backtrace true; *)
Printexc.record_backtrace true;
Arg.parse_dynamic arg_list set_command usage;
let module MC = (val !mc_module : OPTIONS) in
if ( !tafile = "" ) then
......
src/querybuilder.ml
View file @ b32d83ce
type expression =
| Constant of int
| Variable of int
| ConstVariable of int
| Clock of int
| Array of int * expression list
| Sum of expression * expression
| Product of expression * expression
| Substraction of expression * expression
| Division of expression * expression
open Uta
type atomic_guard =
| GuardLeq of expression * expression
......
src/timedAutomaton.ml
View file @ b32d83ce
This diff is collapsed.
src/timedAutomatonBuilder.c
View file @ b32d83ce
......@@ -349,6 +349,7 @@ void
TimedAutomatonBuilder::visitVariable(variable_t &var)
{
CAMLparam0();
CAMLlocal1(indices);
type_t varType = var.uid.getType();
// a clock
......@@ -387,7 +388,7 @@ TimedAutomatonBuilder::visitVariable(variable_t &var)
// raise a warning on urgent and broadcast channels, which are not supported by TiAMo
if (varType.is(Constants::URGENT))
{
caml_failwith("Broadcast channels are not supported by TiAMo");
caml_failwith("Urgent channels are not supported by TiAMo");
}
else if (varType.is(Constants::BROADCAST))
{
......@@ -421,7 +422,6 @@ TimedAutomatonBuilder::visitVariable(variable_t &var)
}
else
{
assert(caml_named_value("cb_register_global_array_name"));
caml_callback(*caml_named_value("cb_register_global_array_name"),
caml_copy_string(var.uid.getName().c_str()));
}
......@@ -431,7 +431,6 @@ TimedAutomatonBuilder::visitVariable(variable_t &var)
// BEWARE of the order: top-most in the type = right-most in the declaration
// then use this vector to iterate over the cells of the array and declare them as
// regular variables with (possible several pairs of) square brackets []
// TODO we also need to represent such multi-dimensional array as expressions in Ocaml
std::vector<int> multiSize;
type_t currentType = varType;
while (currentType.isArray())
......@@ -451,18 +450,26 @@ TimedAutomatonBuilder::visitVariable(variable_t &var)
bool index_is_zero = true;
do
{
std::stringstream cellName;
cellName << var.uid.getName();
for (int i = 0; i != index.size(); ++i)
// std::stringstream cellName;
// cellName << var.uid.getName();
// for (int i = 0; i != index.size(); ++i)
// {
// cellName << "[" << index[i] << "]";
// }
indices = caml_callback(*caml_named_value("cb_empty_list"), Val_unit);
for (auto it = index.rbegin(); it != index.rend(); ++it)
{
cellName << "[" << index[i] << "]";
indices = caml_callback2(*caml_named_value("cb_build_list"),
Val_int(*it),
indices);
}
if (is_channel)
{
// declare current cell as a regular channel
caml_callback(*caml_named_value("cb_register_channel_array_cell"),
caml_copy_string(cellName.str().c_str()));
caml_callback2(*caml_named_value("cb_register_channel_array_cell"),
caml_copy_string(var.uid.getName().c_str()),
indices);
}
else
{
......@@ -481,15 +488,17 @@ TimedAutomatonBuilder::visitVariable(variable_t &var)
// declare current cell as a regular global variable
if (is_const)
{
caml_callback2(*caml_named_value("cb_register_global_const_array_cell"),
caml_copy_string(cellName.str().c_str()),
caml_callback3(*caml_named_value("cb_register_global_const_array_cell"),
caml_copy_string(var.uid.getName().c_str()),
indices,
Val_int(cellValue));
}
else
{
assert(caml_named_value("cb_register_global_array_cell"));
caml_callback2(*caml_named_value("cb_register_global_array_cell"),
caml_copy_string(cellName.str().c_str()),
caml_callback3(*caml_named_value("cb_register_global_array_cell"),
caml_copy_string(var.uid.getName().c_str()),
indices,
Val_int(cellValue));
}
}
......
src/uta.ml
View file @ b32d83ce
......@@ -2,59 +2,194 @@ 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
type expression =
| Constant of int
| Variable of int
| ConstVariable of int
| Clock of int
| ClockArray of int * expression list
| Array of int * expression list
| ConstArray of int * expression list
| Sum of expression * expression
| Product of expression * expression
| Substraction of expression * expression
| Division of expression * expression
module type VARCONTEXT =
functor (Vars : sig type var_t type array_t val cell2var : array_t -> int list -> var_t end) ->
sig
type var_t = Vars.var_t
type arr_t = Vars.array_t
type t =
{
index2var : (int,var_t) Hashtbl.t;
var2index : (var_t,int) Hashtbl.t;
index2array : (int,arr_t) Hashtbl.t;
array2index : (arr_t,int) Hashtbl.t;
cells2vars : (int * int list, int) Hashtbl.t;
mutable nextVarIndex : int;
mutable nextArrayIndex : int;
}
val create : unit -> t
val index_of_var : t -> var_t -> int
val var_of_index : t -> int -> var_t
val mem : t -> var_t -> bool
val index_of_array : t -> arr_t -> int
val array_of_index : t -> int -> arr_t
val arraymem : t -> arr_t -> bool
(* array index -> indices -> corresponding var index *)
val index_of_cell : t -> int -> int list -> int
val add : t -> var_t -> int
val add_array : t -> arr_t -> unit
val add_cell : t -> arr_t -> int list -> int
val size : t -> int
val iter : t -> (var_t -> int -> unit) -> unit
end
module VarContextFunctor : VARCONTEXT =
functor (Vars : sig type var_t type array_t val cell2var : array_t -> int list -> var_t end) ->
struct
type var_t = Vars.var_t
type arr_t = Vars.array_t
type t =
{
index2var : (int,var_t) Hashtbl.t;
var2index : (var_t,int) Hashtbl.t;
index2array : (int,arr_t) Hashtbl.t;
array2index : (arr_t,int) Hashtbl.t;
cells2vars : (int * int list, int) Hashtbl.t;
mutable nextVarIndex : int;
mutable nextArrayIndex : int;
}
let create () =
{
index2var = Hashtbl.create 16;
var2index = Hashtbl.create 16;
index2array = Hashtbl.create 16;
array2index = Hashtbl.create 16;
cells2vars = Hashtbl.create 16;
nextVarIndex = 0;
nextArrayIndex = 0;
}
let index_of_var vc var =
Hashtbl.find vc.var2index var
let var_of_index vc ind =
Hashtbl.find vc.index2var ind
let mem vc var =
Hashtbl.mem vc.var2index var
let index_of_array vc arr =
Hashtbl.find vc.array2index arr
let array_of_index vc ind =
Hashtbl.find vc.index2array ind
let arraymem vc arr =
Hashtbl.mem vc.array2index arr
let index_of_cell vc arrayId indices =
Hashtbl.find vc.cells2vars (arrayId,indices)
let add vc varName =
if (Hashtbl.mem vc.var2index varName) then (
raise Var_already_defined
);
let index = vc.nextVarIndex in
vc.nextVarIndex <- vc.nextVarIndex + 1;
Hashtbl.add vc.index2var index varName;
Hashtbl.add vc.var2index varName index;
index
let add_array vc arrayName =
if (Hashtbl.mem vc.array2index arrayName) then (
raise Var_already_defined
);
let index = vc.nextArrayIndex in
vc.nextArrayIndex <- vc.nextArrayIndex + 1;
Hashtbl.add vc.index2array index arrayName;
Hashtbl.add vc.array2index arrayName index
let add_cell vc arrayName indices =
let arrayIndex = Hashtbl.find vc.array2index arrayName in
let cellVar = Vars.cell2var arrayName indices in
let cellIndex = add vc cellVar in
Hashtbl.add vc.cells2vars (arrayIndex,indices) cellIndex;
cellIndex
let size vc = Hashtbl.length vc.var2index
let iter vc f = Hashtbl.iter f vc.var2index
end
module StringArrayVars =
struct
type var_t = string
type array_t = string
let cell2var arrayName indices =
List.fold_left (fun s -> fun i -> s ^ (string_of_int i)) arrayName indices
end
module VarContext = VarContextFunctor(StringArrayVars)
module ScopeStringArrayVars =
struct
type var_t = int option * string
type array_t = int option * string
let cell2var (procRef,arrayName) indices =
procRef, (List.fold_left (fun s -> fun i -> s ^ (string_of_int i)) arrayName indices)
end
module ScopeVarContext =
struct
include VarContextFunctor(ScopeStringArrayVars)
(* read all elements, by prepending the process name (if any) to the
* variable and array names
*)
let _prepend_procName procs s = function
| None -> s
| Some i -> procs.(i) ^ "." ^ s
(* Convert the ScopeVarContext.t to VarContext.t, by prepending the process
* names to variables and clocks. We just extract these elements from the
* hash tables, along with their indices, so as to reinsert them in the
* same order in the new VarContext. These contexts are only for pretty
* printing and have no role in simulation.
*)
let to_vc : t -> string array -> VarContext.t = fun svc -> fun procs ->
let result = VarContext.create () in
let prep = _prepend_procName procs in
(* Variable names *)
let varList =
List.sort compare
(Hashtbl.fold (fun (p,v) index acc -> (index, prep v p)::acc) svc.var2index []) in
List.iter (fun (_,name) -> let _ = VarContext.add result name in ()) varList;
(* Array names *)
let arrList =
List.sort compare
(Hashtbl.fold (fun (p,v) index acc -> (index, prep v p)::acc) svc.array2index []) in
List.iter (fun (_,name) -> VarContext.add_array result name) arrList;
(* Do not forget the mapping from cells to vars *)
{ result with VarContext.cells2vars = svc.cells2vars }
end
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