Permalink
Browse files

safe mode

  • Loading branch information...
1 parent 7b8ded9 commit 3bdb5f68831f4108213f50fa341659e1c2aa0b86 Krivine committed Jul 16, 2012
Showing with 137 additions and 62 deletions.
  1. +28 −0 .paths
  2. +104 −60 Error/safe.ml
  3. +3 −1 dataStructures/safeHeap.ml
  4. +1 −1 simulation/run.ml
  5. +1 −0 siteGraphs/species.ml
View
28 .paths
@@ -63,3 +63,31 @@ models/cflows/none_only
models/cflows/none_only/expected-output
models/cflows/weak_only
models/cflows/weak_only/expected-output
+models/cflows
+models/cflows/abc
+models/cflows/abc/expected-output
+models/cflows/abc-cflow
+models/cflows/abc-cflow/expected-output
+models/cflows/abc-pert
+models/cflows/abc-pert/expected-output
+models/cflows/agents_without_sites
+models/cflows/agents_without_sites/expected-output
+models/cflows/cube
+models/cflows/cube/expected-output
+models/cflows/link_passing
+models/cflows/link_passing/expected-output
+models/cflows/link_swapping
+models/cflows/link_swapping/expected-output
+models/cflows/none_only
+models/cflows/none_only/expected-output
+models/cflows/observables
+models/cflows/side-effects1
+models/cflows/side-effects1/expected-output
+models/cflows/side-effects2
+models/cflows/side-effects2/expected-output
+models/cflows/side-effects3
+models/cflows/side-effects3/expected-output
+models/cflows/side-effects4
+models/cflows/side-effects4/expected-output
+models/cflows/weak_only
+models/cflows/weak_only/expected-output
View
@@ -25,69 +25,113 @@ and obs = { label : string; expr : Dynamics.variable }
exception Invariant_violation of string
-let check_invariants state counter env =
+type check_options = {rule_act : bool ; lifts : bool ; unary : bool}
+
+let check n =
+ let check_options = {rule_act = false ; lifts = false ; unary = false} in
+ let check_options =
+ if (n land 1) = 1 then {check_options with rule_act = true}
+ else check_options
+ in
+ let check_options =
+ if (n land 2) = 2 then {check_options with lifts = true}
+ else check_options
+ in
+ let check_options =
+ if (n land 4) = 4 then {check_options with unary = true}
+ else check_options
+ in
+ check_options
+
+let check_invariants check_opt state counter env =
try
- Hashtbl.iter (*checking rule activities are OK*)
- (fun r_id rule ->
- let x = Random_tree.find r_id state.activity_tree in
- let a2,a1 = State.eval_activity rule state counter env in
- let alpha = Num.float_of_num (Num.add a2 a1) in
- if x < alpha then
- if (IntSet.mem r_id state.silenced || Random_tree.is_infinite r_id state.activity_tree) then ()
- else
- let msg = Printf.sprintf "Activity of rule %s is underapproximated (%f < %f)" (Environment.rule_of_num r_id env) x alpha in
- raise (Invariant_violation msg)
- else
- ()
- ) state.rules ;
- SiteGraph.fold
- (fun i u_i _ -> (*checking graph lifts are OK*)
- let _ =
- Node.fold_dep
- (fun j (int_j,lnk_j) lifts_base ->
- if j=0 then
- begin
- let str = Environment.site_of_id (Node.name u_i) 0 env in
- if str <> "_" then raise (Invariant_violation "Site 0 should be '_'") ;
- lnk_j
- end
+ if check_opt.rule_act then
+ begin
+ Hashtbl.iter (*checking rule activities are OK*)
+ (fun r_id rule ->
+ let x = Random_tree.find r_id state.activity_tree in
+ let a2,a1 = State.eval_activity rule state counter env in
+ let alpha = Num.float_of_num (Num.add a2 a1) in
+ if x < alpha then
+ if (IntSet.mem r_id state.silenced || Random_tree.is_infinite r_id state.activity_tree) then ()
+ else
+ let msg = Printf.sprintf "Activity of rule %s is underapproximated (%f < %f)" (Environment.rule_of_num r_id env) x alpha in
+ raise (Invariant_violation msg)
else
- begin
- LiftSet.fold
- (fun inj _ ->
- if Injection.is_trashed inj then
- let (r_id,cc_id) = Injection.get_coordinate inj in
+ ()
+ ) state.rules
+ end ;
+
+ if check_opt.lifts then
+ begin
+ SiteGraph.fold
+ (fun i u_i _ -> (*checking graph lifts are OK*)
+ let _ =
+ Node.fold_dep
+ (fun j (int_j,lnk_j) lifts_base ->
+ if j=0 then
+ begin
+ let str = Environment.site_of_id (Node.name u_i) 0 env in
+ if str <> "_" then raise (Invariant_violation "Site 0 should be '_'") ;
+ lnk_j
+ end
+ else
+ begin
+ LiftSet.fold
+ (fun inj _ ->
+ if Injection.is_trashed inj then
+ let (r_id,cc_id) = Injection.get_coordinate inj in
+ if IntSet.mem r_id state.silenced then ()
+ else
+ raise (Invariant_violation "Injection is thrashed but is still pointed at") ;
+ if not (LiftSet.mem inj lifts_base) then
+ raise
+ (Invariant_violation
+ (
+ Printf.sprintf "Injection (%d,%d) is missing in site '_' of node %d" ((fun (x,y)->x) (Injection.get_coordinate inj)) ((fun (x,y)->y) (Injection.get_coordinate inj)) j
+ )
+ )
+ ) lnk_j () ;
+ LiftSet.fold
+ (fun inj _ ->
+ if Injection.is_trashed inj then
+ let (r_id,cc_id) = Injection.get_coordinate inj in
if IntSet.mem r_id state.silenced then ()
else
- raise (Invariant_violation "Injection is thrashed but is still pointed at") ;
- if not (LiftSet.mem inj lifts_base) then
- raise
- (Invariant_violation
- (
- Printf.sprintf "Injection (%d,%d) is missing in site '_' of node %d" ((fun (x,y)->x) (Injection.get_coordinate inj)) ((fun (x,y)->y) (Injection.get_coordinate inj)) j
- )
- )
- ) lnk_j () ;
- LiftSet.fold
- (fun inj _ ->
- if Injection.is_trashed inj then
- let (r_id,cc_id) = Injection.get_coordinate inj in
- if IntSet.mem r_id state.silenced then ()
- else
- raise (Invariant_violation "Injection is thrashed but is still pointed at") ;
- if not (LiftSet.mem inj lifts_base) then
- raise
- (Invariant_violation
- (
- Printf.sprintf "Injection (%d,%d) is missing in site '_' of node %d" ((fun (x,y)->x) (Injection.get_coordinate inj)) ((fun (x,y)->y) (Injection.get_coordinate inj)) j
- )
- )
- ) int_j () ;
- lifts_base
- end
- ) u_i (LiftSet.empty())
- in
- ()
- ) state.graph ()
+ raise (Invariant_violation "Injection is thrashed but is still pointed at") ;
+ if not (LiftSet.mem inj lifts_base) then
+ raise
+ (Invariant_violation
+ (
+ Printf.sprintf "Injection (%d,%d) is missing in site '_' of node %d" ((fun (x,y)->x) (Injection.get_coordinate inj)) ((fun (x,y)->y) (Injection.get_coordinate inj)) j
+ )
+ )
+ ) int_j () ;
+ lifts_base
+ end
+ ) u_i (LiftSet.empty())
+ in
+ ()
+ ) state.graph ()
+ end ;
+
+ if check_opt.unary then
+ begin
+ let ar = Array.init (Array.length state.nl_injections) (fun i -> 0) in
+ Array.iteri
+ (fun r_id injprod_hp_opt ->
+ (*let _ = try Environment.unary_rule_of_num r_id env with Not_found -> raise (Invariant_violation (Printf.sprintf "Rule %d is not unary" r_id))
+ in*)
+ match injprod_hp_opt with
+ | None -> ()
+ | Some injprod_hp ->
+ let n = InjProdHeap.size injprod_hp in
+ ar.(r_id) <- n
+ ) state.nl_injections ;
+ Printf.fprintf stderr "%E " (Counter.time counter) ;
+ Array.iteri (fun _ n -> Printf.fprintf stderr "%d " n ) ar ;
+ Printf.fprintf stderr "\n" ;
+ end
+
with
| Invariant_violation msg -> (Parameter.debugModeOn := true; State.dump state counter env ; Printf.fprintf stderr "%s\n" msg ; exit (-1))
@@ -1,4 +1,5 @@
open LargeArray
+(**Heap with no fragmentation and an equality test for content*)
module type Content =
sig
@@ -89,7 +90,8 @@ module Make(C:Content) =
let gc h f =
let collect = ref [] in
- GenArray.iteri (fun i content -> if f content then collect := i::!collect) ;
+ GenArray.iteri
+ (fun i content_opt -> match content_opt with None -> () | Some content -> if f content then collect := i::!collect) h.ar ;
List.fold_left (fun h i -> remove i h) h !collect
exception Is_present
View
@@ -97,7 +97,7 @@ let event state (*grid*) story_profiling event_list counter plot env =
else state
in
- if !Parameter.safeModeOn then Safe.check_invariants state counter env ;
+ if !Parameter.safeModeOn then Safe.check_invariants (Safe.check 4) state counter env ;
(****************END POSITIVE UPDATE*****************)
View
@@ -34,6 +34,7 @@ let print desc spec env =
) spec.nodes (0,0)
in
()
+
let to_dot hr palette k cpt spec desc env =
let rand_rgb () =

0 comments on commit 3bdb5f6

Please sign in to comment.