Commit 29546c2e authored by mcolange's avatar mcolange

Use the new Dbm interface.

parent c1c13d3d
......@@ -3,7 +3,7 @@ open Options
open Printf
open Reachability
open TimedAutomaton
open Udbml
open Dbm
(** For Arg.align to properly display help messages, do not forget to make them
* start with a space.
......@@ -77,12 +77,13 @@ let execute tafile qfile =
let module WO = WO_tmp(Uta_ds) in
let module Abs = (val !Options.abstraction : UTA_ABSTRACTION) in
let module Incl = (val !Options.inclusion : UTA_INCLUSION) in
let module Reach = Reachability(Uautomaton)(WO(Uautomaton.Dbm))(Abs)(Incl) in
let module Reach = Reachability(Uautomaton)(WO(Uautomaton.MDbm))(Abs)(Incl) in
match (Reach.reach ta) with
| true -> Log.info "reachable!\n"
| false -> Log.info "not reachable...\n"
let main() =
(* Printexc.record_backtrace true; *)
Arg.parse arguments anon_arguments usage;
if ( !tafile = "" ) then
(
......
open Reachability
open TimedAutomaton
open Udbml
open Dbm
module Uautomaton : TIMED_AUTOMATON with type MDbm.dbm_t = Udbml.Dbm.t
= GenericUAutomaton(UDbm)
type ta_discrete = Uautomaton.timed_automaton * Uautomaton.discrete_state
module type UTA_ABSTRACTION =
ABSTRACTION with type arg_t = ta_discrete
and type dbm_t := Uautomaton.Dbm.t
and type dbm_t := Uautomaton.MDbm.Dbm.t
module type UTA_INCLUSION =
INCLUSION with type arg_t = ta_discrete
and type dbm_t := Uautomaton.Dbm.t
and type dbm_t := Uautomaton.MDbm.Dbm.t
module type UTA_WALK_ORDER =
functor (Key : Hashtbl.HashedType with type t = Uautomaton.discrete_state) ->
functor (Dbm : GEN_IDBM) ->
functor (Dbm : BIG_IDBM) ->
WALK_ORDER with type key = Uautomaton.discrete_state
and type dbm_t := Dbm.t
and type dbm_t := Dbm.Dbm.t
module Uta_ds : Hashtbl.HashedType with type t = Uautomaton.discrete_state =
struct
......
......@@ -51,7 +51,7 @@ end
*)
module ID_abstraction (TA : TIMED_AUTOMATON) :
ABSTRACTION with type arg_t = TA.timed_automaton * TA.discrete_state
and type dbm_t := TA.Dbm.t =
and type dbm_t := TA.MDbm.Dbm.t =
struct
type arg_t = TA.timed_automaton * TA.discrete_state
......@@ -60,9 +60,9 @@ end
(** LU abstraction
*)
module Extra_LU (TA : TIMED_AUTOMATON) :
module Extra_LU (TA : TIMED_AUTOMATON with type MDbm.dbm_t = Udbml.Dbm.t) :
ABSTRACTION with type arg_t = TA.timed_automaton * TA.discrete_state
and type dbm_t := TA.Dbm.t =
and type dbm_t := TA.MDbm.Dbm.t =
struct
type arg_t = TA.timed_automaton * TA.discrete_state
......@@ -70,7 +70,7 @@ struct
let extrapolate zone (ta, loc) =
let (lbounds, ubounds) = LUC.lu_bounds ta loc in
TA.Dbm.extrapolate_lu_bounds zone lbounds ubounds
Udbml.Dbm.extrapolate_lu_bounds zone lbounds ubounds
end
......@@ -91,11 +91,11 @@ end
(** Vanilla inclusion *)
module Inclusion (TA : TIMED_AUTOMATON) :
INCLUSION with type arg_t = TA.timed_automaton * TA.discrete_state
and type dbm_t := TA.Dbm.t =
and type dbm_t := TA.MDbm.Dbm.t =
struct
type arg_t = TA.timed_automaton * TA.discrete_state
let inclusion _ = TA.Dbm.leq
let inclusion _ = TA.MDbm.Dbm.leq
end
(** Smart inclusion test, based on (insert reference here)
......@@ -106,9 +106,9 @@ end
* and Z'_{x,y} < Z_{x,y}
* and Z'_{x,y} + (<, - L_y) < Z_{x,0}
*)
module Sri (TA : TIMED_AUTOMATON) :
module Sri (TA : TIMED_AUTOMATON with type MDbm.dbm_t = Udbml.Dbm.t) :
INCLUSION with type arg_t = TA.timed_automaton * TA.discrete_state
and type dbm_t := TA.Dbm.t =
and type dbm_t := TA.MDbm.Dbm.t =
struct
type arg_t = TA.timed_automaton * TA.discrete_state
......@@ -116,7 +116,7 @@ struct
let inclusion (ta, loc) z1 z2 =
let (lbounds, ubounds) = LUC.lu_bounds ta loc in
TA.Dbm.closure_leq lbounds ubounds z1 z2
Udbml.Dbm.closure_leq lbounds ubounds z1 z2
end
(** An abstract type for the walk order of a graph *)
......@@ -158,15 +158,15 @@ end
*)
module Walk_Order (Cont : WAIT_CONTAINER)
(Key : Hashtbl.HashedType)
(Dbm : GEN_IDBM)
: WALK_ORDER with type key = Key.t and type dbm_t := Dbm.t =
(BDbm : Dbm.BIG_IDBM)
: WALK_ORDER with type key = Key.t and type dbm_t := BDbm.Dbm.t =
struct
module KeyHashtbl = Hashtbl.Make(Key)
type dbm_list = Dbm.t list ref
type dbm_list = BDbm.Dbm.t list ref
type key = KeyHashtbl.key
type t = dbm_list KeyHashtbl.t * (key * Dbm.t) Cont.t
type t = dbm_list KeyHashtbl.t * (key * BDbm.Dbm.t) Cont.t
let create () = (KeyHashtbl.create 1000, Cont.create ())
......@@ -218,16 +218,17 @@ module Walk_BFS = Walk_Order (Queue)
module TA_RG_WALK =
functor (TA : TIMED_AUTOMATON) ->
functor (WO : WALK_ORDER with type key = TA.discrete_state
and type dbm_t := TA.Dbm.t) ->
and type dbm_t := TA.MDbm.Dbm.t) ->
functor (ABS : ABSTRACTION
with type arg_t = TA.timed_automaton * TA.discrete_state
and type dbm_t := TA.Dbm.t) ->
and type dbm_t := TA.MDbm.Dbm.t) ->
functor (COMP : INCLUSION
with type arg_t = TA.timed_automaton * TA.discrete_state
and type dbm_t := TA.Dbm.t) ->
and type dbm_t := TA.MDbm.Dbm.t) ->
struct
module Dbm = TA.Dbm
module Dbm = TA.MDbm.Dbm
module Fed = TA.MDbm.Fed
(** Auxiliary function that computes the list of successors of an
* extended state.
......@@ -238,19 +239,20 @@ struct
let apply_transition (sloc, szone) succs_list trans =
let (source, guard, resets, target) = TA.transition_fields ta trans in
assert(TA.is_state_equal sloc source);
let result_zone = Dbm.copy szone in
Dbm.intersect result_zone guard;
if (Dbm.is_empty result_zone) then
let result_zone = Dbm.to_fed (Dbm.copy szone) in
Fed.intersect result_zone guard;
if (Fed.is_empty result_zone) then
succs_list
else (
ClockSet.iter (fun c -> Dbm.update_value result_zone c 0) resets;
ClockSet.iter (fun c -> Fed.update_value result_zone c 0) resets;
if (not (TA.is_urgent_or_committed ta target)) then (
Dbm.up result_zone );
Dbm.intersect result_zone (TA.invariant_of_discrete_state ta target);
if (Dbm.is_empty result_zone) then
Fed.up result_zone );
Fed.intersect result_zone (TA.invariant_of_discrete_state ta target);
if (Fed.is_empty result_zone) then
succs_list
else (
ABS.extrapolate result_zone (ta, target);
let dbm_list = Fed.to_dbm result_zone in
List.iter (fun z -> ABS.extrapolate z (ta, target)) dbm_list;
(*
Printf.printf "Computed transition\n";
TA.print_extended_state stdout ta (loc, zone);
......@@ -258,7 +260,7 @@ struct
TA.print_extended_state stdout ta (target, result_zone);
Printf.printf "\n";
*)
(target, result_zone) :: succs_list
List.fold_left (fun l -> fun z -> (target, z)::l) succs_list dbm_list
)
)
in
......@@ -313,13 +315,13 @@ end
module Reachability =
functor (TA : TIMED_AUTOMATON) ->
functor (WO : WALK_ORDER with type key = TA.discrete_state
and type dbm_t := TA.Dbm.t) ->
and type dbm_t := TA.MDbm.Dbm.t) ->
functor (ABS : ABSTRACTION
with type arg_t = TA.timed_automaton * TA.discrete_state
and type dbm_t := TA.Dbm.t) ->
and type dbm_t := TA.MDbm.Dbm.t) ->
functor (COMP : INCLUSION
with type arg_t = TA.timed_automaton * TA.discrete_state
and type dbm_t := TA.Dbm.t) ->
and type dbm_t := TA.MDbm.Dbm.t) ->
struct
module Walker = TA_RG_WALK(TA)(WO)(ABS)(COMP)
......
......@@ -6,7 +6,7 @@ open Uta
module type TIMED_AUTOMATON =
sig
module Dbm : IDBM
module MDbm : BIG_IDBM
type timed_automaton
type discrete_state
......@@ -17,12 +17,12 @@ sig
val hash_discrete_state : discrete_state -> int
val initial_discrete_state : timed_automaton -> discrete_state
(* does it belong here? If so, so does type for extended_state... *)
val initial_extended_state : timed_automaton -> discrete_state * Dbm.t
val initial_extended_state : timed_automaton -> discrete_state * MDbm.Dbm.t
val transitions_from : timed_automaton -> discrete_state -> transition list
val transition_fields : timed_automaton -> transition ->
(discrete_state * Dbm.t * ClockSet.t * discrete_state)
val guard_of_transition : timed_automaton -> transition -> Dbm.t
val invariant_of_discrete_state : timed_automaton -> discrete_state -> Dbm.t
(discrete_state * MDbm.Dbm.t * ClockSet.t * discrete_state)
val guard_of_transition : timed_automaton -> transition -> MDbm.Dbm.t
val invariant_of_discrete_state : timed_automaton -> discrete_state -> MDbm.Dbm.t
val is_urgent_or_committed : timed_automaton -> discrete_state -> bool
val is_target : timed_automaton -> discrete_state -> bool
val lu_bounds : timed_automaton -> discrete_state -> int array -> int array -> unit
......@@ -30,7 +30,8 @@ sig
val print_discrete_state : 'b BatIO.output -> timed_automaton -> discrete_state -> unit
val print_transition : 'b BatIO.output -> timed_automaton -> transition -> unit
val print_timed_automaton : 'b BatIO.output -> timed_automaton -> unit
val print_extended_state : 'b BatIO.output -> timed_automaton -> (discrete_state * Dbm.t) -> unit
val print_extended_state : 'b BatIO.output -> timed_automaton -> (discrete_state * MDbm.Dbm.t) -> unit
val from_file : string -> string -> ?scale:int -> ?enlarge:int -> unit -> timed_automaton
end
module type TIMED_GAME =
......@@ -43,7 +44,7 @@ end
module GenericUAutomaton (BDbm : BIG_IDBM) =
struct
module MDbm = BDbm
module Dbm = BDbm.Dbm
(** In contrast with Uta.expression used in the parser, the variables here are indexed
......
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