Rule consistency or duplications¶

Here are the background types and functions we can use to represent the obligations and artifacts in these examples.

In [1]:

type obligations = {
  sing_a_song: bool;
  do_a_dance: bool;
}

type employee = {
  name : string;
  arrival_time : int;
  obligations : obligations;
}

type state = {
  emp: employee;
  meeting_time: int;
}

let on_time st =
  st.emp.arrival_time <= st.meeting_time

let is_late st =
  not (on_time st)

Out[1]:

type obligations = { sing_a_song : bool; do_a_dance : bool; }
type employee = {
  name : string;
  arrival_time : Z.t;
  obligations : obligations;
}
type state = { emp : employee; meeting_time : Z.t; }
val on_time : state -> bool = <fun>
val is_late : state -> bool = <fun>

Now for a particular rules we can represent this modules, which have a common structure.

Try this!

In [2]:

(* Employee E must sing a song
   if E is late for a meeting for n minutes
   and n is greater than 3*)

module Rule0 = struct

 let c1 st =
  is_late st

 let c2 st =
  st.emp.arrival_time - st.meeting_time > 3

 let cs st =
  c1 st && c2 st

 let s st =
  st.emp.obligations.sing_a_song

 let rule st =
  s st <== cs st

end

Out[2]:

module Rule0 :
  sig
    val c1 : state -> bool
    val c2 : state -> bool
    val cs : state -> bool
    val s : state -> bool
    val rule : state -> bool
  end

Try this!

In [3]:

(*
  Employee E must sing a song
  if E is late for a meeting for n minutes
  and n is greater than 1
*)

module Rule1 = struct

 let c1 st =
  is_late st

 let c2 st =
  st.emp.arrival_time - st.meeting_time > 1

 let cs st =
  c1 st && c2 st

 let s st =
  st.emp.obligations.sing_a_song

 let rule st =
  s st <== cs st

end

Out[3]:

module Rule1 :
  sig
    val c1 : state -> bool
    val c2 : state -> bool
    val cs : state -> bool
    val s : state -> bool
    val rule : state -> bool
  end

We can ask questions about these rules such as if the statements overlap using Imandra's instance mechanism:

Try this!

In [4]:

(* Do Rule0's and Rule1's conditions overlap? *)

instance (fun st -> (Rule0.c1 st) && (Rule1.c1 st))

Out[4]:

- : state -> bool = <fun>
module CX : sig val st : state end

Instance (after 0 steps, 0.019s):
let st : state =
  {emp =
   {name = "!0!"; arrival_time = 0;
    obligations = {sing_a_song = false; do_a_dance = false}};
   meeting_time = (-1)}

Instance

call graph
proof

Loading..

proof attempt

ground_instances:

0

definitions:

0

inductions:

0

search_time:

0.019s

details:

Expand

smt_stats:

num checks:	1
arith assert lower:	1
arith tableau max rows:	1
arith tableau max columns:	4
arith pivots:	1
rlimit count:	331
mk clause:	16
datatype occurs check:	1
mk bool var:	22
decisions:	2
seq num reductions:	1
propagations:	2
datatype accessor ax:	4
arith num rows:	1
datatype constructor ax:	4
num allocs:	6850118
final checks:	1
added eqs:	23
del clause:	8
time:	0.009000
memory:	16.290000
max memory:	16.690000

Expand

start[0.019s]
  let (_x_0 : bool)
      = not (( :var_0: ).emp.arrival_time <= ( :var_0: ).meeting_time)
  in _x_0 && _x_0

simplify

into:	not (( :var_0: ).emp.arrival_time <= ( :var_0: ).meeting_time)
expansions:	[]
rewrite_steps:
forward_chaining:

Sat (Some let st : state = {emp = {name = "!0!"; arrival_time = (Z.of_nativeint (0n)); obligations = {sing_a_song = false; do_a_dance = false}}; meeting_time = (Z.of_nativeint (-1n))} )

Loading..

Try this!

In [5]:

(* Employee E must sing a song
   if E is late for a meeting for n minutes
   and n is less than 3*)

module Rule2 = struct

 let c1 st =
  is_late st

 let c2 st =
  st.emp.arrival_time - st.meeting_time < 3

 let cs st =
  c1 st && c2 st

 let s st =
  st.emp.obligations.sing_a_song

 let rule st =
  s st <== cs st

end

Out[5]:

module Rule2 :
  sig
    val c1 : state -> bool
    val c2 : state -> bool
    val cs : state -> bool
    val s : state -> bool
    val rule : state -> bool
  end

Try this!

In [6]:

(* Employee E must do a dance
   if E is late for a meeting for n minutes
   and n is greater than 3*)

module Rule3 = struct

 let c1 st =
  is_late st

 let c2 st =
  st.emp.arrival_time - st.meeting_time > 3

 let cs st =
  c1 st && c2 st

 let s st =
  st.emp.obligations.do_a_dance

 let rule st =
  s st <== cs st

end

Out[6]:

module Rule3 :
  sig
    val c1 : state -> bool
    val c2 : state -> bool
    val cs : state -> bool
    val s : state -> bool
    val rule : state -> bool
  end

Try this!

In [7]:

(* Employee E must NOT sing a song
   if E is late for a meeting for n minutes
   and n is greater than 1 *)

module Rule3 = struct

 let c1 st =
  is_late st

 let c2 st =
  st.emp.arrival_time - st.meeting_time > 1

 let cs st =
  c1 st && c2 st

 let s st =
  not (st.emp.obligations.sing_a_song)

 let rule st =
  s st <== cs st

end

Out[7]:

module Rule3 :
  sig
    val c1 : state -> bool
    val c2 : state -> bool
    val cs : state -> bool
    val s : state -> bool
    val rule : state -> bool
  end

Try this!

In [8]:

(* Employee E must not sing a song
   if E is late for a meeting for n minutes
   and n is greater than 3 *)

module Rule4 = struct

 let c1 st =
  is_late st

 let c2 st =
  st.emp.arrival_time - st.meeting_time > 3

 let cs st =
  c1 st && c2 st

 let s st =
  not (st.emp.obligations.sing_a_song)

 let rule st =
  s st <== cs st

end

Out[8]:

module Rule4 :
  sig
    val c1 : state -> bool
    val c2 : state -> bool
    val cs : state -> bool
    val s : state -> bool
    val rule : state -> bool
  end

Try this!

In [9]:

(* Employee E must do a dance
   if E is late for a meeting for n minutes
   and n is greater than 3 *)

module Rule5 = struct

 let c1 st =
  is_late st

 let c2 st =
  st.emp.arrival_time - st.meeting_time > 1

 let cs st =
  c1 st && c2 st

 let s st =
  st.emp.obligations.do_a_dance

 let rule st =
  s st <== cs st

end

Out[9]:

module Rule5 :
  sig
    val c1 : state -> bool
    val c2 : state -> bool
    val cs : state -> bool
    val s : state -> bool
    val rule : state -> bool
  end

Try this!

In [10]:

(* Employee E must sing a song
   if E is late for a meeting for n minutes
   and n is less than 3 *)

module Rule6 = struct

 let c1 st =
  is_late st

 let c2 st =
  st.emp.arrival_time - st.meeting_time < 3

 let cs st =
  c1 st && c2 st

 let s st =
  st.emp.obligations.sing_a_song

 let rule st =
  s st <== cs st

end

Out[10]:

module Rule6 :
  sig
    val c1 : state -> bool
    val c2 : state -> bool
    val cs : state -> bool
    val s : state -> bool
    val rule : state -> bool
  end

Try this!

In [11]:

(* Employee E must not sing a song
   if E is late for a meeting for n minutes
   and n is greater than 1 *)

module Rule7 = struct

 let c1 st =
  is_late st

 let c2 st =
  st.emp.arrival_time - st.meeting_time > 1

 let cs st =
  c1 st && c2 st

 let s st =
  not (st.emp.obligations.sing_a_song)

 let rule st =
  s st <== cs st

end

Out[11]:

module Rule7 :
  sig
    val c1 : state -> bool
    val c2 : state -> bool
    val cs : state -> bool
    val s : state -> bool
    val rule : state -> bool
  end

Try this!

In [12]:

(* Employee E must not sing a song
   if E is late for a meeting for n minutes
   and n is less than 3 *)

module Rule8 = struct

 let c1 st =
  is_late st

 let c2 st =
  st.emp.arrival_time - st.meeting_time < 3

 let cs st =
  c1 st && c2 st

 let s st =
  not (st.emp.obligations.sing_a_song)

 let rule st =
  s st <== cs st

end

Out[12]:

module Rule8 :
  sig
    val c1 : state -> bool
    val c2 : state -> bool
    val cs : state -> bool
    val s : state -> bool
    val rule : state -> bool
  end

Let's pose some queries about the relationships of these rules¶

Try this!

In [13]:

(* Do the conditions of rules 0 and 1 overlap? *)

instance (fun st -> Rule0.cs st && Rule1.cs st)

Out[13]:

- : state -> bool = <fun>
module CX : sig val st : state end

Instance (after 0 steps, 0.018s):
let st : state =
  {emp =
   {name = "!0!"; arrival_time = 0;
    obligations = {sing_a_song = false; do_a_dance = false}};
   meeting_time = (-4)}

Instance

call graph
proof

Loading..

proof attempt

ground_instances:

0

definitions:

0

inductions:

0

search_time:

0.018s

details:

Expand

smt_stats:

num checks:	1
arith assert lower:	3
arith tableau max rows:	1
arith tableau max columns:	4
arith pivots:	1
rlimit count:	577
mk clause:	16
datatype occurs check:	1
mk bool var:	24
decisions:	2
seq num reductions:	1
propagations:	2
datatype accessor ax:	4
arith num rows:	1
datatype constructor ax:	4
num allocs:	14642280
final checks:	1
added eqs:	23
del clause:	8
time:	0.008000
memory:	17.880000
max memory:	18.260000

Expand

start[0.018s]
  let (_x_0 : int) = ( :var_0: ).emp.arrival_time in
  let (_x_1 : int) = ( :var_0: ).meeting_time in
  let (_x_2 : bool) = not (_x_0 <= _x_1) in
  let (_x_3 : int) = _x_0 - _x_1 in
  _x_2 && (_x_3 > 3) && (_x_2 && (_x_3 > 1))

simplify

into:	let (_x_0 : int) = ( :var_0: ).emp.arrival_time in let (_x_1 : int) = ( :var_0: ).meeting_time in let (_x_2 : int) = _x_0 + (-1) * _x_1 in not (_x_0 <= _x_1) && not (_x_2 <= 3) && not (_x_2 <= 1)
expansions:	[]
rewrite_steps:
forward_chaining:

Sat (Some let st : state = {emp = {name = "!0!"; arrival_time = (Z.of_nativeint (0n)); obligations = {sing_a_song = false; do_a_dance = false}}; meeting_time = (Z.of_nativeint (-4n))} )

digraph "proof" {
p_5 [label="Start (let (_x_0 : int) = ( :var_0: ).emp.arrival_time in\l       let (_x_1 : int) = ( :var_0: ).meeting_time in\l       let (_x_2 : bool) = not (_x_0 \<= _x_1) in\l       let (_x_3 : int) = _x_0 - _x_1 in\l       _x_2 && (_x_3 \> 3) && (_x_2 && (_x_3 \> 1)) :time 0.018s)",shape=box,style=filled,fontname="courier",fontsize=14];
p_5 -> p_4 [label=""];
p_4 [label="Simplify (let (_x_0 : int) = ( :var_0: ).emp.arrival_time in\l          let (_x_1 : int) = ( :var_0: ).meeting_time in\l          let (_x_2 : int) = _x_0 + (-1) * _x_1 in\l          not (_x_0 \<= _x_1) && not (_x_2 \<= 3) && not (_x_2 \<= 1)\l          :expansions [] :rw [] :fc [])",shape=box,style=filled,fontname="courier",fontsize=14];
p_4 -> p_3 [label=""];
p_3 [label="Sat (Some let st : state =\l  \{emp =\l   \{name = \"!0!\"; arrival_time = (Z.of_nativeint (0n));\l    obligations = \{sing_a_song = false; do_a_dance = false\}\};\l   meeting_time = (Z.of_nativeint (-4n))\}\l)",shape=box,style=filled,fontname="courier",fontsize=14];
}

Loading..

Try this!

In [14]:

(* Do the statements of rules 0 and 1 overlap? *)

instance (fun st -> Rule0.s st && Rule1.s st)

Out[14]:

- : state -> bool = <fun>
module CX : sig val st : state end

Instance (after 0 steps, 0.017s):
let st : state =
  {emp =
   {name = ""; arrival_time = 0;
    obligations = {sing_a_song = true; do_a_dance = false}};
   meeting_time = 0}

Instance

call graph
proof

Loading..

proof attempt

ground_instances:

0

definitions:

0

inductions:

0

search_time:

0.017s

details:

Expand

smt_stats:

num checks:	1
rlimit count:	119
mk bool var:	1
eliminated applications:	3
num allocs:	22838437
final checks:	1
time:	0.008000
memory:	18.020000
max memory:	18.270000

Expand

start[0.017s]
  let (_x_0 : bool) = ( :var_0: ).emp.obligations.sing_a_song in _x_0 && _x_0

simplify
into:
( :var_0: ).emp.obligations.sing_a_song
expansions:
[]
rewrite_steps:
forward_chaining:
Sat (Some let st : state = {emp = {name = ""; arrival_time = (Z.of_nativeint (0n)); obligations = {sing_a_song = true; do_a_dance = false}}; meeting_time = (Z.of_nativeint (0n))} )

Loading..

Try this!

In [15]:

(* We can encode these as checks on rules.
   We prefix with `v` if `verify` should be used, else with `i` if `instance` should be used. *)

let v_check_1 r1_cs r1_s r2_cs r2_s st =
  r1_s st = r2_s st && r1_cs st = r2_cs st

Out[15]:

val v_check_1 :
  ('a -> 'b) -> ('a -> 'c) -> ('a -> 'b) -> ('a -> 'c) -> 'a -> bool = <fun>

Try this!

In [16]:

(* For example, we can do check1 for Rule0 and Rule0 *)

verify (fun st -> v_check_1 Rule0.cs Rule0.s Rule0.cs Rule0.s st)

Out[16]:

- : state -> bool = <fun>

Proved

proof
call graph

proof

ground_instances:

0

definitions:

0

inductions:

0

search_time:

0.016s

details:

Expand

smt_stats:

rlimit count:	7
num allocs:	32625989
time:	0.007000
memory:	18.420000
max memory:	18.420000

Expand

```
start[0.016s] true
```
Unsat

Loading..

Try this!

In [17]:

(* And similarly for Rule0 and Rule1 *)

verify (fun st -> v_check_1 Rule0.cs Rule0.s Rule1.cs Rule1.s st)

Out[17]:

- : state -> bool = <fun>
module CX : sig val st : state end

Counterexample (after 0 steps, 0.019s):
let st : state =
  {emp =
   {name = "!0!"; arrival_time = 0;
    obligations = {sing_a_song = false; do_a_dance = false}};
   meeting_time = (-2)}

Refuted

call graph
proof

Loading..

proof attempt

ground_instances:

0

definitions:

0

inductions:

0

search_time:

0.019s

details:

Expand

smt_stats:

num checks:	1
arith assert lower:	2
arith tableau max rows:	1
arith tableau max columns:	4
arith pivots:	1
rlimit count:	733
mk clause:	26
datatype occurs check:	1
mk bool var:	26
arith assert upper:	1
decisions:	3
seq num reductions:	1
propagations:	10
conflicts:	1
datatype accessor ax:	4
arith num rows:	1
datatype constructor ax:	4
num allocs:	45617351
final checks:	1
added eqs:	23
del clause:	8
time:	0.010000
memory:	18.660000
max memory:	19.020000

Expand

start[0.019s]
  let (_x_0 : int) = ( :var_0: ).emp.arrival_time in
  let (_x_1 : int) = ( :var_0: ).meeting_time in
  let (_x_2 : bool) = not (_x_0 <= _x_1) in
  let (_x_3 : int) = _x_0 - _x_1 in
  (_x_2 && (_x_3 > 3)) = (_x_2 && (_x_3 > 1))

simplify

into:	let (_x_0 : int) = ( :var_0: ).emp.arrival_time in let (_x_1 : int) = ( :var_0: ).meeting_time in let (_x_2 : bool) = not (_x_0 <= _x_1) in let (_x_3 : int) = _x_0 + (-1) * _x_1 in (_x_2 && not (_x_3 <= 3)) = (_x_2 && not (_x_3 <= 1))
expansions:	[]
rewrite_steps:
forward_chaining:

Sat (Some let st : state = {emp = {name = "!0!"; arrival_time = (Z.of_nativeint (0n)); obligations = {sing_a_song = false; do_a_dance = false}}; meeting_time = (Z.of_nativeint (-2n))} )

digraph "proof" {
p_13 [label="Start (let (_x_0 : int) = ( :var_0: ).emp.arrival_time in\l       let (_x_1 : int) = ( :var_0: ).meeting_time in\l       let (_x_2 : bool) = not (_x_0 \<= _x_1) in\l       let (_x_3 : int) = _x_0 - _x_1 in\l       (_x_2 && (_x_3 \> 3)) = (_x_2 && (_x_3 \> 1)) :time 0.019s)",shape=box,style=filled,fontname="courier",fontsize=14];
p_13 -> p_12 [label=""];
p_12 [label="Simplify (let (_x_0 : int) = ( :var_0: ).emp.arrival_time in\l          let (_x_1 : int) = ( :var_0: ).meeting_time in\l          let (_x_2 : bool) = not (_x_0 \<= _x_1) in\l          let (_x_3 : int) = _x_0 + (-1) * _x_1 in\l          (_x_2 && not (_x_3 \<= 3)) = (_x_2 && not (_x_3 \<= 1))\l          :expansions [] :rw [] :fc [])",shape=box,style=filled,fontname="courier",fontsize=14];
p_12 -> p_11 [label=""];
p_11 [label="Sat (Some let st : state =\l  \{emp =\l   \{name = \"!0!\"; arrival_time = (Z.of_nativeint (0n));\l    obligations = \{sing_a_song = false; do_a_dance = false\}\};\l   meeting_time = (Z.of_nativeint (-2n))\}\l)",shape=box,style=filled,fontname="courier",fontsize=14];
}

Loading..

Try this!

In [18]:

(* Now let's consider check2: statements the same but conditions different (overlapping) *)
(* We do this with two checks, one universal and one existential: *)

let v_check2 r1_cs r1_s r2_cs r2_s st =
 r1_s st = r2_s st

let i_check2 r1_cs r1_s r2_cs r2_s st =
 r1_cs st && r2_cs st

Out[18]:

val v_check2 : 'a -> ('b -> 'c) -> 'd -> ('b -> 'c) -> 'b -> bool = <fun>
val i_check2 : ('a -> bool) -> 'b -> ('a -> bool) -> 'c -> 'a -> bool = <fun>

Try this!

In [19]:

(* Let's check condition 2 for Rule0 and Rule1 -- we see it holds! *)

verify (fun st -> v_check2 Rule0.cs Rule0.s Rule1.cs Rule2.s st)
instance (fun st -> i_check2 Rule0.cs Rule0.s Rule1.cs Rule2.s st)

Out[19]:

- : state -> bool = <fun>
- : state -> bool = <fun>
module CX : sig val st : state end

Proved

proof
call graph

proof

ground_instances:

0

definitions:

0

inductions:

0

search_time:

0.016s

details:

Expand

smt_stats:

rlimit count:	32
num allocs:	59668086
time:	0.008000
memory:	19.160000
max memory:	19.160000

Expand

```
start[0.016s] true
```
simplify
into:
true
expansions:
[]
rewrite_steps:
forward_chaining:
Unsat

Loading..

Instance (after 0 steps, 0.018s):
let st : state =
  {emp =
   {name = "!0!"; arrival_time = 0;
    obligations = {sing_a_song = false; do_a_dance = false}};
   meeting_time = (-4)}

Instance

call graph
proof

Loading..

proof attempt

ground_instances:

0

definitions:

0

inductions:

0

search_time:

0.018s

details:

Expand

smt_stats:

num checks:	1
arith assert lower:	3
arith tableau max rows:	1
arith tableau max columns:	4
arith pivots:	1
rlimit count:	583
mk clause:	16
datatype occurs check:	1
mk bool var:	24
decisions:	2
seq num reductions:	1
propagations:	2
datatype accessor ax:	4
arith num rows:	1
datatype constructor ax:	4
num allocs:	77404793
final checks:	1
added eqs:	23
del clause:	8
time:	0.009000
memory:	19.360000
max memory:	19.760000

Expand

start[0.018s]
  let (_x_0 : int) = ( :var_0: ).emp.arrival_time in
  let (_x_1 : int) = ( :var_0: ).meeting_time in
  let (_x_2 : bool) = not (_x_0 <= _x_1) in
  let (_x_3 : int) = _x_0 - _x_1 in
  _x_2 && (_x_3 > 3) && (_x_2 && (_x_3 > 1))

simplify

into:	let (_x_0 : int) = ( :var_0: ).emp.arrival_time in let (_x_1 : int) = ( :var_0: ).meeting_time in let (_x_2 : int) = _x_0 + (-1) * _x_1 in not (_x_0 <= _x_1) && not (_x_2 <= 3) && not (_x_2 <= 1)
expansions:	[]
rewrite_steps:
forward_chaining:

Sat (Some let st : state = {emp = {name = "!0!"; arrival_time = (Z.of_nativeint (0n)); obligations = {sing_a_song = false; do_a_dance = false}}; meeting_time = (Z.of_nativeint (-4n))} )

digraph "proof" {
p_19 [label="Start (let (_x_0 : int) = ( :var_0: ).emp.arrival_time in\l       let (_x_1 : int) = ( :var_0: ).meeting_time in\l       let (_x_2 : bool) = not (_x_0 \<= _x_1) in\l       let (_x_3 : int) = _x_0 - _x_1 in\l       _x_2 && (_x_3 \> 3) && (_x_2 && (_x_3 \> 1)) :time 0.018s)",shape=box,style=filled,fontname="courier",fontsize=14];
p_19 -> p_18 [label=""];
p_18 [label="Simplify (let (_x_0 : int) = ( :var_0: ).emp.arrival_time in\l          let (_x_1 : int) = ( :var_0: ).meeting_time in\l          let (_x_2 : int) = _x_0 + (-1) * _x_1 in\l          not (_x_0 \<= _x_1) && not (_x_2 \<= 3) && not (_x_2 \<= 1)\l          :expansions [] :rw [] :fc [])",shape=box,style=filled,fontname="courier",fontsize=14];
p_18 -> p_17 [label=""];
p_17 [label="Sat (Some let st : state =\l  \{emp =\l   \{name = \"!0!\"; arrival_time = (Z.of_nativeint (0n));\l    obligations = \{sing_a_song = false; do_a_dance = false\}\};\l   meeting_time = (Z.of_nativeint (-4n))\}\l)",shape=box,style=filled,fontname="courier",fontsize=14];
}

Loading..

Try this!

In [20]:

(* Let's check condition 2 for Rule0 and Rule2 -- we see it does not hold! *)

verify (fun st -> v_check2 Rule0.cs Rule0.s Rule2.cs Rule2.s st)
instance (fun st -> i_check2 Rule0.cs Rule0.s Rule2.cs Rule2.s st)

Out[20]:

- : state -> bool = <fun>
- : state -> bool = <fun>

Proved

proof
call graph

proof

ground_instances:

0

definitions:

0

inductions:

0

search_time:

0.016s

details:

Expand

smt_stats:

rlimit count:	32
num allocs:	94505637
time:	0.007000
memory:	19.560000
max memory:	19.760000

Expand

```
start[0.016s] true
```
simplify
into:
true
expansions:
[]
rewrite_steps:
forward_chaining:
Unsat

Loading..

Unsatisfiable

proof
call graph

proof

ground_instances:

0

definitions:

0

inductions:

0

search_time:

0.018s

details:

Expand

smt_stats:

num checks:	1
arith assert lower:	2
arith tableau max rows:	1
arith tableau max columns:	4
rlimit count:	508
mk clause:	16
mk bool var:	24
arith assert upper:	1
seq num reductions:	1
conflicts:	1
datatype accessor ax:	4
arith conflicts:	1
arith num rows:	1
datatype constructor ax:	4
num allocs:	116639780
added eqs:	15
time:	0.009000
memory:	19.740000
max memory:	20.160000

Expand

start[0.018s]
  let (_x_0 : int) = ( :var_0: ).emp.arrival_time in
  let (_x_1 : int) = ( :var_0: ).meeting_time in
  let (_x_2 : bool) = not (_x_0 <= _x_1) in
  let (_x_3 : int) = _x_0 - _x_1 in
  _x_2 && (_x_3 > 3) && (_x_2 && (_x_3 < 3))

simplify

into:	let (_x_0 : int) = ( :var_0: ).emp.arrival_time in let (_x_1 : int) = ( :var_0: ).meeting_time in let (_x_2 : int) = _x_0 + (-1) * _x_1 in not (_x_0 <= _x_1) && not (_x_2 <= 3) && not (3 <= _x_2)
expansions:	[]
rewrite_steps:
forward_chaining:

Unsat

Loading..

Try this!

In [21]:

(* Now let's do check 7: contrary statements with same conditions *)

let v_check7 r1_cs r1_s r2_cs r2_s st =
 (r1_s st <==> not(r2_s st)) && (r1_cs st = r2_cs st)

Out[21]:

val v_check7 :
  ('a -> 'b) -> ('a -> bool) -> ('a -> 'b) -> ('a -> bool) -> 'a -> bool =
  <fun>

Try this!

In [22]:

(* We'll check this for Rule0 and Rule 4 *)

verify (fun st -> v_check7 Rule0.cs Rule0.s Rule4.cs Rule4.s st)

Out[22]:

- : state -> bool = <fun>

Proved

proof
call graph

proof

ground_instances:

0

definitions:

0

inductions:

0

search_time:

0.017s

details:

Expand

smt_stats:

rlimit count:	126
num allocs:	138364849
time:	0.008000
memory:	20.120000
max memory:	20.160000

Expand

```
start[0.017s] true
```
simplify
into:
true
expansions:
[]
rewrite_steps:
forward_chaining:
Unsat

Loading..

Try this!

In [23]:

(* Now let's check it for Rule0 and Rule5 -- we see it's not true! *)

verify (fun st -> v_check7 Rule0.cs Rule0.s Rule5.cs Rule5.s st)

Out[23]:

- : state -> bool = <fun>
module CX : sig val st : state end

Counterexample (after 0 steps, 0.020s):
let st : state =
  {emp =
   {name = "!0!"; arrival_time = 0;
    obligations = {sing_a_song = false; do_a_dance = false}};
   meeting_time = 38}

Refuted

call graph
proof

Loading..

proof attempt

ground_instances:

0

definitions:

0

inductions:

0

search_time:

0.020s

details:

Expand

smt_stats:

num checks:	1
arith tableau max rows:	1
arith tableau max columns:	4
rlimit count:	989
mk clause:	33
datatype occurs check:	1
mk bool var:	28
decisions:	3
seq num reductions:	1
propagations:	8
datatype accessor ax:	4
arith num rows:	1
datatype constructor ax:	4
num allocs:	164455119
final checks:	1
added eqs:	23
del clause:	8
time:	0.010000
memory:	20.350000
max memory:	20.710000

Expand

start[0.020s]
  let (_x_0 : employee) = ( :var_0: ).emp in
  let (_x_1 : obligations) = _x_0.obligations in
  let (_x_2 : int) = _x_0.arrival_time in
  let (_x_3 : int) = ( :var_0: ).meeting_time in
  let (_x_4 : bool) = not (_x_2 <= _x_3) in
  let (_x_5 : int) = _x_2 - _x_3 in
  (_x_1.sing_a_song = not _x_1.do_a_dance)
  && ((_x_4 && (_x_5 > 3)) = (_x_4 && (_x_5 > 1)))

simplify

into:	let (_x_0 : employee) = ( :var_0: ).emp in let (_x_1 : obligations) = _x_0.obligations in let (_x_2 : int) = _x_0.arrival_time in let (_x_3 : int) = ( :var_0: ).meeting_time in let (_x_4 : bool) = not (_x_2 <= _x_3) in let (_x_5 : int) = _x_2 + (-1) * _x_3 in (_x_1.sing_a_song = not _x_1.do_a_dance) && ((_x_4 && not (_x_5 <= 3)) = (_x_4 && not (_x_5 <= 1)))
expansions:	[]
rewrite_steps:
forward_chaining:

Sat (Some let st : state = {emp = {name = "!0!"; arrival_time = (Z.of_nativeint (0n)); obligations = {sing_a_song = false; do_a_dance = false}}; meeting_time = (Z.of_nativeint (38n))} )

digraph "proof" {
p_31 [label="Start (let (_x_0 : employee) = ( :var_0: ).emp in\l       let (_x_1 : obligations) = _x_0.obligations in\l       let (_x_2 : int) = _x_0.arrival_time in\l       let (_x_3 : int) = ( :var_0: ).meeting_time in\l       let (_x_4 : bool) = not (_x_2 \<= _x_3) in\l       let (_x_5 : int) = _x_2 - _x_3 in\l       (_x_1.sing_a_song = not _x_1.do_a_dance)\l       && ((_x_4 && (_x_5 \> 3)) = (_x_4 && (_x_5 \> 1))) :time 0.020s)",shape=box,style=filled,fontname="courier",fontsize=14];
p_31 -> p_30 [label=""];
p_30 [label="Simplify (let (_x_0 : employee) = ( :var_0: ).emp in\l          let (_x_1 : obligations) = _x_0.obligations in\l          let (_x_2 : int) = _x_0.arrival_time in\l          let (_x_3 : int) = ( :var_0: ).meeting_time in\l          let (_x_4 : bool) = not (_x_2 \<= _x_3) in\l          let (_x_5 : int) = _x_2 + (-1) * _x_3 in\l          (_x_1.sing_a_song = not _x_1.do_a_dance)\l          && ((_x_4 && not (_x_5 \<= 3)) = (_x_4 && not (_x_5 \<= 1)))\l          :expansions [] :rw [] :fc [])",shape=box,style=filled,fontname="courier",fontsize=14];
p_30 -> p_29 [label=""];
p_29 [label="Sat (Some let st : state =\l  \{emp =\l   \{name = \"!0!\"; arrival_time = (Z.of_nativeint (0n));\l    obligations = \{sing_a_song = false; do_a_dance = false\}\};\l   meeting_time = (Z.of_nativeint (38n))\}\l)",shape=box,style=filled,fontname="courier",fontsize=14];
}

Loading..

Let's look at a region decomp of a particular rule to get examples of its distinct behaviours.

Try this!

In [24]:

let rule5 = Rule5.rule;;

Out[24]:

val rule5 : state -> bool = <fun>

Try this!

In [25]:

Modular_decomp.top "rule5";;

Out[25]:

- : Modular_decomp_intf.decomp_ref = <abstr>

Voronoi (3 of 3)
Table

{
  "regions": [
    {
      "constraints": [ "st.meeting_time >= st.emp.arrival_time" ],
      "region": {
        "constraints": [ "st.meeting_time >= st.emp.arrival_time" ],
        "invariant": "F = true"
      },
      "groups": [],
      "label": "2",
      "weight": 1
    },
    {
      "constraints": [ "st.emp.arrival_time > st.meeting_time" ],
      "region": null,
      "groups": [
        {
          "constraints": [
            "st.emp.arrival_time > st.meeting_time",
            "(st.emp.arrival_time - st.meeting_time) > 1"
          ],
          "region": {
            "constraints": [
              "st.emp.arrival_time > st.meeting_time",
              "(st.emp.arrival_time - st.meeting_time) > 1"
            ],
            "invariant": "F = st.emp.obligations.do_a_dance"
          },
          "groups": [],
          "label": "1.2",
          "weight": 1
        },
        {
          "constraints": [
            "st.emp.arrival_time > st.meeting_time",
            "(st.emp.arrival_time - st.meeting_time) <= 1"
          ],
          "region": {
            "constraints": [
              "st.emp.arrival_time > st.meeting_time",
              "(st.emp.arrival_time - st.meeting_time) <= 1"
            ],
            "invariant": "F = true"
          },
          "groups": [],
          "label": "1.1",
          "weight": 1
        }
      ],
      "label": "",
      "weight": 2
    }
  ]
}

Regions details

No group selected.

Concrete regions are numbered
Unnumbered regions are groups whose children share a particular constraint
Click on a region to view its details
Double click on a region to zoom in on it
Shift+double click to zoom out
Hit escape to reset back to the top

decomp of (rule5 st

Reg_id

Constraints

Invariant

2

```
st.emp.arrival_time <= st.meeting_time
```

true

1

not (st.emp.arrival_time <= st.meeting_time)

not (st.emp.arrival_time - st.meeting_time > 1)

true

0

not (st.emp.arrival_time <= st.meeting_time)

st.emp.arrival_time - st.meeting_time > 1

st.emp.obligations.do_a_dance

into:	( :var_0: ).emp.obligations.sing_a_song
expansions:	[]
rewrite_steps:
forward_chaining: