ksuenaga / hybridpdr Goto Github PK

This should be done in prior to #5

CHECKING WHETHER THE FOLLOWING IS UNSAT:
prim((and (<= x 1.0) (>= x (/ 1.0 2.0))))
AND
[[(y, x); (x, (* y (- 1.0)))] & (>= y 0.0)]prim((and (<= y 0.0) (>= y 0.0) (<= x (- (/ 5.0 4.0))) (>= x (- (/ 5.0 4.0)))))

is decided to be Unsat, while there is a counterexample (x,y) = (1.0, 0.6).

CHECKING WHETHER THE FOLLOWING IS UNSAT:
prim(true)
AND
<[(y, x); (x, (* y (- 1.0)))] & (>= y 0.0)>prim((and (<= y 0.0)
(<= x (/ 5433.0 3125.0))
(>= x (/ 5433.0 3125.0))
(<= y (/ 990679.0 1000000.0))
(>= y (/ 990679.0 1000000.0))))
is_satisfiable_conjunction: primdyn: eliminating
Result: Unsat

newframes: 0 -> [("1", (and (<= x (/ 1.0 2.0)) (>= x (/ 1.0 2.0))));
("2", false)]
1 -> [("1", (and (<= x 1.0) (<= x (/ 1.0 2.0)))); ("2", (<= x 1.0))]
2 -> [("1", (<= x 1.0)); ("2", (<= x 1.0))]
3 -> [("1", (<= x 1.0)); ("2", (<= x 1.0))]

remove_cti: Current cexs are:
At location "2", at frame 2, CE: (and (<= y (- (/ 5433.0 3125.0)))
(>= y (- (/ 5433.0 3125.0)))
(<= x (/ 990679.0 1000000.0))
(>= x (/ 990679.0 1000000.0)))
remove_cti: processing At location "2", at frame 2, CE: (and (<= y (- (/ 5433.0 3125.0)))
(>= y (- (/ 5433.0 3125.0)))
(<= x (/ 990679.0 1000000.0))
(>= x (/ 990679.0 1000000.0)))
is_continous: false
eframe: [("1", false);
("2",
(or (and (<= y (- (/ 5433.0 3125.0)))
(>= y (- (/ 5433.0 3125.0)))
(<= x (/ 990679.0 1000000.0))
(>= x (/ 990679.0 1000000.0)))
false))
]
wpframe: [("1",
<[(y, x); (x, (* y (- 1.0)))] & (>= y 0.0)>prim((and (<= y 0.0)
(<= y (- (/ 5433.0 3125.0)))
(>= y (- (/ 5433.0 3125.0)))
(<= x (/ 990679.0 1000000.0))
(>= x (/ 990679.0 1000000.0)))));
("2",
<[(y, x); (x, (* y (- 1.0)))] & (<= y 0.0)>prim((and (>= y 0.0) false)))
]
preframe: [("1", prim((and (<= x 1.0) (<= x (/ 1.0 2.0)))));
("2", prim((<= x 1.0)))]
t1:prim((and (<= x 1.0) (<= x (/ 1.0 2.0))))
t2:<[(y, x); (x, (* y (- 1.0)))] & (>= y 0.0)>prim((and (<= y 0.0)
(<= y (- (/ 5433.0 3125.0)))
(>= y (- (/ 5433.0 3125.0)))
(<= x (/ 990679.0 1000000.0))
(>= x (/ 990679.0 1000000.0))))
CHECKING WHETHER THE FOLLOWING IS UNSAT:
prim((and (<= x 1.0) (<= x (/ 1.0 2.0))))
AND
<[(y, x); (x, (* y (- 1.0)))] & (>= y 0.0)>prim((and (<= y 0.0)
(<= y (- (/ 5433.0 3125.0)))
(>= y (- (/ 5433.0 3125.0)))
(<= x (/ 990679.0 1000000.0))
(>= x (/ 990679.0 1000000.0))))
is_satisfiable_conjunction: primdyn: eliminating
Result: Unsat
t1:prim((<= x 1.0))
t2:<[(y, x); (x, (* y (- 1.0)))] & (<= y 0.0)>prim((and (>= y 0.0) false))
CHECKING WHETHER THE FOLLOWING IS UNSAT:
prim((<= x 1.0))
AND
prim(false)
Result: Unsat
backpropagated to:

from:
[("1", false);
("2",
(or (and (<= y (- (/ 5433.0 3125.0)))
(>= y (- (/ 5433.0 3125.0)))
(<= x (/ 990679.0 1000000.0))
(>= x (/ 990679.0 1000000.0)))
false))
]

The specification is in
http://spaceex.imag.fr/sites/default/files/spaceex_modeling_language_0.pdf
Tools are being developed in
http://spaceex.imag.fr/download-6
including a GUI editor for this modeling language.

We need to deal with this modeling language because
In ARCH competition, which deals with various benchmarks, a benchmark is written in this language.
There seems not OCaml frontend for this modeling language maybe we need to write a library to deal with this language.

Maybe we need to find a way to use Core.

In the dynamics circle.xml:

CHECKING WHETHER THE FOLLOWING IS UNSAT:
prim((<= x 1.0))
AND
[[(y, x); (x, (* y (- 1.0)))] & (<= y 0.0)]prim((not (>= y 0.0)))
Result: Sat with (and (<= y (- 1.0)) (>= y (- 1.0)) (<= x 0.0) (>= x 0.0))
backpropagated to:
At location "2", at frame 1, CE: (and (<= y (- 1.0)) (>= y (- 1.0)) (<= x 0.0) (>= x 0.0))
At location "1", at frame 1, CE: (and (<= y (- (/ 5433.0 3125.0)))
(>= y (- (/ 5433.0 3125.0)))
(<= x (/ 990679.0 1000000.0))
(>= x (/ 990679.0 1000000.0)))
from:
[("1", false);
("2",
(or (and (<= y (- (/ 5433.0 3125.0)))
(>= y (- (/ 5433.0 3125.0)))
(<= x (/ 990679.0 1000000.0))
(>= x (/ 990679.0 1000000.0)))
false))
]

Location 1 of the precond is false, whereas location 2 of the post frame is not false.