Skip to content

Commit

Permalink
Roll back dReach to 3.16.06.02
Browse files Browse the repository at this point in the history
  • Loading branch information
@soonho-tri
soonho-tri committed Jun 28, 2018
1 parent b464262 commit 6fa469f
Show file tree
Hide file tree
Showing 37 changed files with 311 additions and 3,374 deletions.
4 changes: 2 additions & 2 deletions tools/_oasis
View file
Original file line number Diff line number Diff line change
Expand Up @@ -11,7 +11,7 @@ Library basic
BuildTools: ocamlbuild
BuildDepends: batteries
NativeOpt: -passopt -annot
Modules: Type, Checker, Error, Basic, Ode, Value, Vardecl, Vardeclmap, Jump, Jumpmap, Mode, Modemap, Hybrid, Id, Network, Replace, Replacemap, Replaceautmap, Modemapping
Modules: Type, Checker, Error, Basic, Ode, Value, Vardecl, Vardeclmap, Jump, Jumpmap, Mode, Modemap, Hybrid, Id

Library heuristic
Path: ./heuristic
Expand All @@ -25,7 +25,7 @@ Library parsing
BuildTools: ocamlbuild
BuildDepends: basic
NativeOpt: -passopt -annot
Modules: Drh_lexer, Drh_parser, Drh_lexer_networks, Drh_parser_networks
Modules: Drh_lexer, Drh_parser

Library smt2
Path: ./smt2
Expand Down
57 changes: 10 additions & 47 deletions tools/basic/basic.ml
View file
Original file line number Diff line number Diff line change
Expand Up @@ -60,47 +60,6 @@ type exp =
| LetE of ((string * exp) list * formula)
| ForallT of exp * exp * exp * formula

let rec collect_update_assignments_in_formula (f : formula) : (var * formula) Set.t =
match f with
True -> Set.empty
| False -> Set.empty
| Not f' -> collect_update_assignments_in_formula f'
| And fs -> collect_update_assignments_in_formulas fs
| Or fs -> collect_update_assignments_in_formulas fs
| Gt (e1, e2) | Lt (e1, e2) | Ge (e1, e2) | Le (e1, e2) | Eq (e1, e2) | Gtp (e1, e2, _) | Ltp (e1, e2, _) | Gep (e1, e2, _) | Lep (e1, e2, _) | Eqp (e1, e2, _) ->
begin
let vars = contains_update_vars_list [e1;e2] in
match Set.is_empty (contains_update_vars_list [e1;e2]) with
| false -> Set.singleton (Set.choose vars, f)
| true -> Set.empty
end
| Imply (f1, f2) -> collect_update_assignments_in_formulas [f1;f2]
| FVar x -> Set.empty
| ForallT (m, lb, ub, f') -> Set.empty
| LetF _ -> raise TODO
| LetE _ -> raise TODO
and contains_update_vars_list (es : exp list) =
List.reduce Set.union (List.map contains_update_vars es)
and collect_update_assignments_in_formulas (fs : formula list) =
List.reduce Set.union (List.map collect_update_assignments_in_formula fs)
and contains_update_vars (e : exp) : var Set.t = match e with
Var x ->
begin
match String.ends_with x "'" with
| true -> Set.singleton x
| false -> Set.empty
end
| Vec xs -> Set.of_list (List.filter (fun s -> String.ends_with s "'") xs)
| Num _ -> Set.empty
| Neg e' -> contains_update_vars e'
| Add es | Sub es | Mul es -> contains_update_vars_list es
| Div (e1, e2) | Pow (e1, e2) | Atan2 (e1, e2) | Min (e1, e2) | Max (e1, e2) -> contains_update_vars_list [e1;e2]
| Ite (f, e1, e2) -> raise TODO
| Sqrt e' | Abs e' | Log e' | Exp e' | Sin e' | Cos e' | Tan e'
| Asin e' | Acos e' | Atan e' | Asinh e' | Acosh e' | Atanh e' | Matan e'
| Sinh e' | Cosh e' | Tanh e' | Safesqrt e' -> contains_update_vars e'
| Integral (n, t, x0s, flow) -> raise TODO

let rec collect_vars_in_formula (f : formula) : var Set.t =
match f with
True -> Set.empty
Expand Down Expand Up @@ -138,7 +97,6 @@ and collect_vars_in_exp (e : exp) : var Set.t = match e with
| Sinh e' | Cosh e' | Tanh e' | Safesqrt e' -> collect_vars_in_exp e'
| Integral (n, t, x0s, flow) ->
Set.add t (Set.of_list x0s)

let make_or (fs : formula list) =
let reduced_fs_opt = List.fold_left
(fun fs f -> match (fs, f) with
Expand Down Expand Up @@ -611,9 +569,14 @@ let rec print_exp out =
out
xs
| Num n ->
let max_digits10_IEE754_double = 17 in
let res = Printf.sprintf "%0.*g" max_digits10_IEE754_double n in
String.print out res
let str_n = Printf.sprintf "%g" n in
let str_n' =
if String.ends_with str_n "." then
str_n ^ "0"
else
str_n
in
String.print out str_n'
| Neg e' -> print_exps "-" [Num 0.0; e']
| Add el -> print_exps "+" el
| Sub el -> print_exps "-" el
Expand Down Expand Up @@ -707,7 +670,7 @@ and print_formula out =
function
| True -> String.print out "true"
| False -> String.print out "false"
| FVar x -> String.print out x
| FVar x -> String.print out "x"
| Not f -> print_formulas "not" [f]
| And fs -> print_formulas "and" fs
| Or fs -> print_formulas "or" fs
Expand Down Expand Up @@ -866,7 +829,7 @@ and print_infix_formula (out : 'a IO.output) : formula -> unit =
function
| True -> String.print out "true"
| False -> String.print out "false"
| FVar x -> String.print out x
| FVar x -> String.print out "x"
| Not f -> print_infix_formulas "not" [f]
| And fs -> print_infix_formulas "and" fs
| Or fs -> print_infix_formulas "or" fs
Expand Down
17 changes: 0 additions & 17 deletions tools/basic/error.ml
View file
Original file line number Diff line number Diff line change
Expand Up @@ -4,13 +4,6 @@
*)

exception Lex_err of string * int
exception Domain_Mismatch of string
exception Variable_Label_Match of string
exception Variable_Label_Mapping of string
exception Automaton_Not_Found of string
exception Instance_Error of string * string
exception Composition_Error of string
exception Pathgen_Error of string

let linenum = ref 1
let incr_ln () = linenum := !linenum + 1
Expand All @@ -27,14 +20,4 @@ let handle_exn v =
Printf.eprintf ">> syntax error at line %d\n" !linenum
| Arg.Bad s ->
Printf.eprintf ">> file format error: %s\n" s
| Domain_Mismatch s ->
Printf.eprintf ">> domain mismatch: %s\n" s
| Variable_Label_Match s ->
Printf.eprintf ">> variable and name share same identifier: %s\n" s
| Automaton_Not_Found s ->
Printf.eprintf ">> automaton not found: %s\n" s
| Instance_Error (temp, inst) ->
Printf.eprintf ">> unable to instanciate %s: %s not defined.\n" inst temp
| Composition_Error s ->
Printf.eprintf ">> undefined automaton: %s\n" s
| _ -> raise v
89 changes: 15 additions & 74 deletions tools/basic/hybrid.ml
View file
Original file line number Diff line number Diff line change
Expand Up @@ -2,16 +2,13 @@ open Batteries

(* 1. Variable Declaration *)
type vardeclmap = Vardeclmap.t
type labellist = string list

(* 2. Mode *)
type modeId = Mode.id
type numId = int
type mode = Mode.t
type modemap = Modemap.t
type formula = Basic.formula
type exp = Basic.formula
type name = string

(* 3. Init and Goal *)
type init = modeId * formula
Expand All @@ -25,59 +22,23 @@ type t = {varmap: vardeclmap;
init_id: Mode.id;
init_formula: formula;
goals: goals;
ginvs: ginvs;
name: name;
num_id: numId;
labels: labellist}
ginvs: ginvs}


let make (vm, mm, iid, iformula, gs, ginvs, n, nid, ll)
let make (vm, mm, iid, iformula, gs, ginvs)
=
{varmap= vm;
modemap= mm;
init_id = iid;
init_formula = iformula;
goals= gs;
ginvs = ginvs;
name = n;
num_id = nid;
labels = ll}

(*let makep (vm, mm, gs ginvs, n, ll)
=
{varmap= vm;
modemap= mm;
init_id = "";
init_formula = False;
goals= gs;
ginvs = ginvs;
name = n;
labels = ll}*)

let vardeclmap {varmap = var; modemap = mo; init_id = iid; init_formula = ifo; goals = gs; ginvs = g; name = n; num_id = nid; labels = ll } = var

let labellist {varmap = var; modemap = mo; init_id = iid; init_formula = ifo; goals = gs; ginvs = g; name = n; num_id = nid; labels = ll } = ll

let name {varmap = var; modemap = mo; init_id = iid; init_formula = ifo; goals = gs; ginvs = g; name = n; num_id = nid; labels = ll } = n

let modemap {varmap = var; modemap = mo; init_id = iid; init_formula = ifo; goals = gs; ginvs = g; name = n; num_id = nid; labels = ll } = mo

let init_id {varmap = var; modemap = mo; init_id = iid; init_formula = ifo; goals = gs; ginvs = g; name = n; num_id = nid; labels = ll } = iid

let init_formula {varmap = var; modemap = mo; init_id = iid; init_formula = ifo; goals = gs; ginvs = g; name = n; num_id = nid; labels = ll } = ifo

let goals {varmap = var; modemap = mo; init_id = iid; init_formula = ifo; goals = gs; ginvs = g; name = n; num_id = nid; labels = ll } = gs

let ginvs {varmap = var; modemap = mo; init_id = iid; init_formula = ifo; goals = gs; ginvs = g; name = n; num_id = nid; labels = ll } = g

let numid {varmap = var; modemap = mo; init_id = iid; init_formula = ifo; goals = gs; ginvs = g; name = n; num_id = nid; labels = ll } = nid
ginvs = ginvs}

(**
Only used in the parser.
Substitute all the constant variables with their values.
**)

let preprocess (vm, cm, mm, iid, iformula, gs, ginvs, n, nid, ll) : t =
let preprocess (vm, cm, mm, iid, iformula, gs, ginvs) : t =
let subst s =
match Map.mem s cm with
| true ->
Expand All @@ -88,14 +49,11 @@ let preprocess (vm, cm, mm, iid, iformula, gs, ginvs, n, nid, ll) : t =
end
| false -> Basic.Var s
in
let cnt: int ref = ref 0 in
let mm' =
Map.map
(fun m -> begin
cnt := !cnt + 1;
(fun m ->
Mode.make
(Mode.mode_id m,
!cnt,
Mode.time_precision m,
begin
match (Mode.invs_op m) with
Expand All @@ -109,28 +67,23 @@ let preprocess (vm, cm, mm, iid, iformula, gs, ginvs, n, nid, ll) : t =
(Basic.preprocess_formula subst (Jump.guard j),
Jump.precision j,
Jump.target j,
Basic.preprocess_formula subst (Jump.change j),
Jump.label j))
Basic.preprocess_formula subst (Jump.change j)))
(Mode.jumps m),
Map.map
(fun j ->
Jump.makep
(Basic.preprocess_formula subst (Jump.guard j),
Jump.precision j,
Jump.target j,
Basic.preprocess_formula subst (Jump.change j),
Jump.label j))
(Mode.jumpmap m),

0
Basic.preprocess_formula subst (Jump.change j)))
(Mode.jumpmap m)
)
end
)
mm in
let init_formula' = Basic.preprocess_formula subst iformula in
let goals' = List.map (fun (id, goal) -> (id, Basic.preprocess_formula subst goal)) gs in
let ginvs' = List.map (fun ginv -> Basic.preprocess_formula subst ginv) ginvs in
make (vm, mm', iid, init_formula', goals', ginvs', n, nid, ll)
make (vm, mm', iid, init_formula', goals', ginvs')

let adjacent mode_id1 mode_id2 h : bool =
let mode1 = Map.find mode_id1 h.modemap in
Expand All @@ -140,24 +93,16 @@ let print out (hm : t) =
let id_formula_print out (id, f) =
Printf.fprintf out "(%s, %s)" (IO.to_string Id.print id) (IO.to_string Basic.print_formula f)
in
let str_list_print out =
List.print String.print out
in
let print_header out str =
Printf.fprintf out "\n====================%s====================\n" str
Printf.fprintf out "====================\n%s====================" str
in
begin
(* print name *)
print_header out (name hm);
(* print varDecl list *)
print_header out "VarDecl Map";
Vardeclmap.print out hm.varmap;
(* print mode list *)
print_header out "Mode Map";
Modemap.print out hm.modemap;
(* print label list *)
print_header out "Label List";
str_list_print out hm.labels;
(* print init *)
print_header out "Init";
List.print ~first:"" ~sep:"\n" ~last:"\n" id_formula_print out [(hm.init_id, hm.init_formula)];
Expand All @@ -175,7 +120,7 @@ let goal_ids (hm : t) : modeId list
2) the last mode of the path should be an element of the goals of the HM
3) the unrolling step k, should match with the length of the given path
**)
let check_path (hm : t) (path : (string list) option) (k : int) : unit =
let check_path (hm : t) (path : int list option) (k : int) : unit =
let init = hm.init_id in
let goals = goal_ids hm in
match path with
Expand All @@ -184,19 +129,19 @@ let check_path (hm : t) (path : (string list) option) (k : int) : unit =
let first_mode = List.first p in
let last_mode = List.last p in
let len = List.length p in
let path_str = IO.to_string (List.print ~first:"[" ~last:"]" ~sep:", " String.print) p in
let goal_str = IO.to_string (List.print ~first:"[" ~last:"]" ~sep:", " String.print) goals in
let path_str = IO.to_string (List.print ~first:"[" ~last:"]" ~sep:", " Int.print) p in
let goal_str = IO.to_string (List.print ~first:"[" ~last:"]" ~sep:", " Int.print) goals in
match (first_mode = init, List.mem last_mode goals, len = k + 1) with
(true, true, true) -> ()
| (false, _, _) ->
let msg = Printf.sprintf
"The first mode of the given path %s is %s which is different from %s, the initial mode of the given hybrid system model."
"The first mode of the given path %s is %d which is different from %d, the initial mode of the given hybrid system model."
path_str first_mode init
in
raise (Arg.Bad msg)
| (_, false, _) ->
let msg = Printf.sprintf
"The last mode of the given path %s is %s which is not an element of %s, the list of modes in the goal section of the given hybrid system model."
"The last mode of the given path %s is %d which is not an element of %s, the list of modes in the goal section of the given hybrid system model."
path_str last_mode goal_str
in
raise (Arg.Bad msg)
Expand All @@ -208,7 +153,3 @@ let check_path (hm : t) (path : (string list) option) (k : int) : unit =
raise (Arg.Bad msg)
end
| None -> ()




Loading

0 comments on commit 6fa469f

Please sign in to comment.