Commit 0e8708a0 authored by mcolange's avatar mcolange

Add a module that builds a M-bounded automaton from a timed automaton.

parent d8f56437
......@@ -37,6 +37,40 @@ sig
val from_file : string -> string -> ?scale:int -> ?enlarge:int -> unit -> timed_automaton
end
module MBoundedAutomaton (TA : TIMED_AUTOMATON) =
struct
include TA
let bounding_transitions ta state=
let n = VarContext.size (TA.clocks ta) in
let m = TA.global_m_bounds ta in
let rec build_list cl accu =
if (cl = n) then accu
else
let guard = Dbm.UDbm.Dbm.create n in
Dbm.UDbm.Dbm.set_init guard;
Dbm.UDbm.Dbm.constrain guard (0, cl, (-m.(cl)-2, Udbml.Basic_types.DBM_WEAK));
Dbm.UDbm.Dbm.constrain guard (cl, 0, (m.(cl)+2, Udbml.Basic_types.DBM_WEAK));
assert(not(Dbm.UDbm.Dbm.is_empty guard));
build_list (cl+1) ((state, guard, [(cl, m.(cl)+1)], state)::accu)
in
build_list 1 []
let transitions_from ta state =
List.rev_append (TA.transitions_from ta state) (bounding_transitions ta state)
let invariant_of_discrete_state ta state =
let inv = TA.invariant_of_discrete_state ta state in
let n = VarContext.size (TA.clocks ta) in
let m = TA.global_m_bounds ta in
for cl = 0 to n-1 do
Dbm.UDbm.Dbm.constrain inv (cl, 0, (m.(cl) + 2, Udbml.Basic_types.DBM_WEAK))
done;
assert(not(Dbm.UDbm.Dbm.is_empty inv));
inv
end
module type TIMED_GAME =
sig
include TIMED_AUTOMATON
......
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