Skip to content
GitLab
Menu
Projects
Groups
Snippets
/
Help
Help
Support
Community forum
Keyboard shortcuts
?
Submit feedback
Contribute to GitLab
Sign in
Toggle navigation
Menu
Open sidebar
Christian Müller
NIWO
Commits
0f390288
Commit
0f390288
authored
Jan 22, 2019
by
Christian Müller
Browse files
Merge branch 'master' of versioncontrolseidl.in.tum.de:mueller/loopingworkflows
parents
582ced11
2e9e706a
Changes
12
Hide whitespace changes
Inline
Side-by-side
.gitignore
View file @
0f390288
...
...
@@ -31,6 +31,11 @@ build
results/*.ltl
results/*.ppltl
results/*.foltl
results/*.png
results/*.metrics
# aalta
cnf.dimacs
# Z3
lib/com.microsoft.z3.jar
examples/omitting/conference.spec
View file @
0f390288
...
...
@@ -5,19 +5,19 @@ forallmay x:A,p:P
forallmay x:A,p:P
!Conf(x,p) → Assign += (x,p)
forall x:A,p:P,r:R
(Assign(x,p) ∧ O(x,p,r)) → Review += (x,p,r)
(Assign(x,p) ∧ O
racle
(x,p,r)) → Review += (x,p,r)
loop {
forall x:A,
y
:A,p:P,r:R (Assign(x,p) ∧ Review(
y
,p,r)) → Read += (x
,p
,r)
forall x
a
:A,
xb
:A,p:P,r:R (Assign(x
a
,p) ∧ Review(
xb
,p,r)) → Read += (x
a
,r)
forallmay x:A,p:P,r:R (Assign(x,p)) → Review += (x,p,r)
}
Declassify
O(x:A,p:P,r:R): ¬ Conf(xt:A,p:P)
O
racle
(x:A,p:P,r:R): ¬ Conf(x
a
t:A,p:P)
Target
Read(xt:A, rt:R)
Read(x
a
t:A, rt:R)
Causality
...
...
src/main/java/Test.java
View file @
0f390288
...
...
@@ -9,9 +9,9 @@ class Test {
public
static
void
main
(
String
[]
args
)
{
System
.
out
.
println
(
"Test"
);
var
owlform
=
BooleanConstant
.
FALSE
;
BooleanConstant
owlform
=
BooleanConstant
.
FALSE
;
var
checksat
=
LanguageAnalysis
.
isSatisfiable
(
owlform
);
boolean
checksat
=
LanguageAnalysis
.
isSatisfiable
(
owlform
);
System
.
out
.
println
(
checksat
);
}
...
...
src/main/scala/de/tum/workflows/InvariantInspector.scala
0 → 100644
View file @
0f390288
package
de.tum.workflows
import
foltl.FOLTL._
import
blocks.Workflow._
import
Implicits._
import
com.typesafe.scalalogging.LazyLogging
import
de.tum.workflows.foltl.FOTransformers
import
de.tum.workflows.Utils._
import
de.tum.workflows.foltl.Stubborn
import
de.tum.workflows.foltl.Properties
import
java.io.PrintWriter
import
java.io.File
import
de.tum.workflows.blocks.Workflow
import
de.tum.workflows.blocks.Spec
import
de.tum.workflows.foltl.FormulaFunctions
import
de.tum.workflows.toz3.InvariantChecker
import
de.tum.workflows.toz3.InvariantGenerator
import
de.tum.workflows.toz3.InvProperties
import
de.tum.workflows.toz3.Z3QFree
object
InvariantInspector
extends
App
with
LazyLogging
{
def
inspect
(
name
:
String
)
{
logger
.
info
(
s
"Generating $name"
)
val
optspec
=
ExampleWorkflows
.
parseExample
(
name
)
if
(!
optspec
.
isDefined
)
{
logger
.
error
(
s
"Not a valid spec: $name"
)
}
val
spec
=
optspec
.
get
logger
.
info
(
s
"Encoding Spec:\n$spec"
)
def
invariant
=
InvariantGenerator
.
invariantNoninterSingleBS
_
// InvariantGenerator.invariantNoninterStubbornBS _
// InvariantChecker.invariantNoninterStubborn _
// InvariantChecker.invariantAllEqual _
val
(
t
,
(
res
,
dot
))
=
time
{
// InvariantChecker.checkInvariantOnce(spec.w, inv(spec), true)
val
props
=
InvProperties
(
stubborn
=
false
,
eliminateAux
=
true
)
val
(
result
,
graph
,
afterlabels
,
proven
,
dot
,
time
)
=
InvariantChecker
.
checkInvariantFPLabelling
(
spec
,
invariant
(
spec
),
props
)
// non-omitting conference linear inspection
val
lastlabels
=
afterlabels
.
last
val
inv
=
lastlabels
(
2
)
val
emptyinv
=
inv
.
assumeEmpty
(
List
(
"informed"
,
"Read"
,
"Comm"
)).
simplify
()
logger
.
info
(
s
"empty: ${emptyinv.pretty()}"
)
// val auxes = List("O", "choice2")
// Different Os
val
diffos
=
emptyinv
everywhere
{
case
Fun
(
"O"
,
Some
(
t
),
vars
)
=>
Fun
(
s
"O$t"
,
vars
)
}
val
auxes
=
List
(
"Ot1"
,
"Ot2"
)
// val auxes = List()
val
auxless
=
auxes
.
foldLeft
(
diffos
)((
inv
,
p
)
=>
FOTransformers
.
eliminateAuxiliaryPredicate
(
inv
,
p
)
)
val
simped
=
auxless
.
toCNF
.
simplify
()
logger
.
info
(
s
"auxless: ${simped.pretty()}"
)
logger
.
info
(
"Computing with B now"
)
val
withB
=
simped
everywhere
{
case
Fun
(
"Assign"
,
t
,
vars
)
=>
And
(
Fun
(
"Assign"
,
t
,
vars
),
Neg
(
Fun
(
"B"
,
vars
)))
// case Fun("Assign",t,vars) => Fun("B",vars)
}
logger
.
info
(
s
"withB: ${withB.simplify().pretty()}"
)
logger
.
info
(
s
"withB CNF: ${withB.toCNF.simplify().pretty()}"
)
logger
.
info
(
s
"Graph: $graph"
)
logger
.
info
(
s
"Final Invariants:\n${afterlabels.last}"
)
(
result
,
dot
)
}
val
msg
=
s
"Invariant was ${if (res) "" else "
not
"}proven (took $t ms)\n"
write
(
s
"${name}.inv"
,
msg
)
for
((
s
,
i
)
<-
dot
.
zipWithIndex
)
{
write
(
s
"${name}_${i}.dot"
,
s
)
}
}
inspect
(
"nonomitting/conference_linear"
)
// inspect("tests/loopexampleNoOracle")
// generateAllExamples()
}
\ No newline at end of file
src/main/scala/de/tum/workflows/MainInvariants.scala
View file @
0f390288
...
...
@@ -54,6 +54,7 @@ object MainInvariants extends App with LazyLogging {
clear
()
// generateExample("nonomitting/conference")
generateExample
(
"tests/loopexampleNoOracle"
)
generateExample
(
"omitting/conference"
)
// generateExample("tests/loopexampleNoOracle")
// generateAllExamples()
}
\ No newline at end of file
src/main/scala/de/tum/workflows/MainLTL.scala
View file @
0f390288
...
...
@@ -7,6 +7,7 @@ import de.tum.workflows.Utils._
import
de.tum.workflows.foltl.Properties
import
de.tum.workflows.blocks.Spec
import
de.tum.workflows.foltl.FormulaFunctions
import
de.tum.workflows.foltl.FOTransformers
import
de.tum.workflows.owltransformer.OwlTransformer
import
owl.ltl.algorithms.LanguageAnalysis
import
owl.ltl.rewriter.SimplifierFactory
...
...
src/main/scala/de/tum/workflows/foltl/FOTransformers.scala
View file @
0f390288
...
...
@@ -52,17 +52,8 @@ object FOTransformers extends LazyLogging {
def
eliminateAuxiliaryPredicate
(
f
:
Formula
,
AUX
:
String
)
=
{
val
(
quantifiers
,
clauses
)
=
FormulaFunctions
.
toCNFClauses
(
f
)
// Inspect clauses
val
simped
=
for
(
c
<-
clauses
;
removeclause
=
(
for
(
c1
<-
c
if
(
c
.
contains
(
Neg
(
c1
))))
yield
true
)
if
(
removeclause
.
isEmpty
)
)
yield
{
c
}
// TODO: improve
val
form
=
And
.
make
(
simped
.
map
(
Or
.
make
))
val
form
=
And
.
make
(
clauses
.
map
(
Or
.
make
))
val
newform
=
quantifiers
.
foldRight
(
form
)((
q
,
inner
)
=>
if
(
q
.
_1
)
Exists
(
q
.
_2
,
inner
)
else
Forall
(
q
.
_2
,
inner
))
// TODO: add equalities?
...
...
@@ -70,8 +61,8 @@ object FOTransformers extends LazyLogging {
case
Neg
(
Fun
(
AUX
,
_
,
_
))
=>
False
case
Fun
(
AUX
,
_
,
_
)
=>
False
}
repld
.
simplify
()
// TODO: improve runtime here
repld
.
toCNF
.
simplify
()
}
/**
...
...
src/main/scala/de/tum/workflows/foltl/FormulaFunctions.scala
View file @
0f390288
...
...
@@ -7,7 +7,6 @@ import scala.annotation.tailrec
object
FormulaFunctions
extends
LazyLogging
{
def
freeVars
(
t
:
Formula
)
=
{
def
free
(
t
:
Formula
,
bound
:
Set
[
Var
])
:
Set
[
Var
]
=
{
t
match
{
...
...
@@ -31,67 +30,66 @@ object FormulaFunctions extends LazyLogging {
def
simplify
(
t
:
Formula
)
:
Formula
=
{
val
simp
:
PartialFunction
[
Formula
,
Formula
]
=
{
// Push negation inward
case
Neg
(
Or
(
t1
,
t2
))
=>
And
(
Neg
(
t1
),
Neg
(
t2
))
case
Neg
(
And
(
t1
,
t2
))
=>
Or
(
Neg
(
t1
),
Neg
(
t2
))
case
Neg
(
Globally
(
t
))
=>
Finally
(
Neg
(
t
))
case
Neg
(
Finally
(
t
))
=>
Globally
(
Neg
(
t
))
case
Neg
(
Next
(
t
))
=>
Next
(
Neg
(
t
))
case
Neg
(
Forall
(
vars
,
t
))
=>
Exists
(
vars
,
Neg
(
t
))
case
Neg
(
Exists
(
vars
,
t
))
=>
Forall
(
vars
,
Neg
(
t
))
case
Neg
(
Implies
(
t1
,
t2
))
=>
And
(
t1
,
Neg
(
t2
))
case
Neg
(
Or
(
t1
,
t2
))
=>
And
(
Neg
(
t1
),
Neg
(
t2
))
case
Neg
(
And
(
t1
,
t2
))
=>
Or
(
Neg
(
t1
),
Neg
(
t2
))
case
Neg
(
Globally
(
t
))
=>
Finally
(
Neg
(
t
))
case
Neg
(
Finally
(
t
))
=>
Globally
(
Neg
(
t
))
case
Neg
(
Next
(
t
))
=>
Next
(
Neg
(
t
))
case
Neg
(
Forall
(
vars
,
t
))
=>
Exists
(
vars
,
Neg
(
t
))
case
Neg
(
Exists
(
vars
,
t
))
=>
Forall
(
vars
,
Neg
(
t
))
case
Neg
(
Implies
(
t1
,
t2
))
=>
And
(
t1
,
Neg
(
t2
))
// Simple laws
case
Neg
(
True
)
=>
False
case
Neg
(
False
)
=>
True
case
Neg
(
Neg
(
t
))
=>
t
case
Or
(
True
,
t
)
=>
True
case
Or
(
t
,
True
)
=>
True
case
Or
(
False
,
t
)
=>
t
case
Or
(
t
,
False
)
=>
t
case
And
(
False
,
t
)
=>
False
case
And
(
t
,
False
)
=>
False
case
And
(
True
,
t
)
=>
t
case
And
(
t
,
True
)
=>
t
case
Implies
(
False
,
t
)
=>
True
case
Implies
(
True
,
t
)
=>
t
case
Or
(
Neg
(
t1
),
t2
)
if
t1
==
t2
=>
True
case
And
(
Neg
(
t1
),
t2
)
if
t1
==
t2
=>
False
case
Or
(
t1
,
Neg
(
t2
))
if
t1
==
t2
=>
True
case
And
(
t1
,
Neg
(
t2
))
if
t1
==
t2
=>
False
case
Neg
(
True
)
=>
False
case
Neg
(
False
)
=>
True
case
Neg
(
Neg
(
t
))
=>
t
case
Or
(
True
,
t
)
=>
True
case
Or
(
t
,
True
)
=>
True
case
Or
(
False
,
t
)
=>
t
case
Or
(
t
,
False
)
=>
t
case
And
(
False
,
t
)
=>
False
case
And
(
t
,
False
)
=>
False
case
And
(
True
,
t
)
=>
t
case
And
(
t
,
True
)
=>
t
case
Implies
(
False
,
t
)
=>
True
case
Implies
(
True
,
t
)
=>
t
case
Or
(
Neg
(
t1
),
t2
)
if
t1
==
t2
=>
True
case
And
(
Neg
(
t1
),
t2
)
if
t1
==
t2
=>
False
case
Or
(
t1
,
Neg
(
t2
))
if
t1
==
t2
=>
True
case
And
(
t1
,
Neg
(
t2
))
if
t1
==
t2
=>
False
// left-trees
case
And
(
And
(
t1
,
t2
),
t3
)
=>
And
(
t1
,
And
(
t2
,
t3
))
case
Or
(
Or
(
t1
,
t2
),
t3
)
=>
Or
(
t1
,
Or
(
t2
,
t3
))
case
And
(
And
(
t1
,
t2
),
t3
)
=>
And
(
t1
,
And
(
t2
,
t3
))
case
Or
(
Or
(
t1
,
t2
),
t3
)
=>
Or
(
t1
,
Or
(
t2
,
t3
))
// equal things in tree
case
And
(
t1
,
t2
)
if
t1
==
t2
=>
t1
case
Or
(
t1
,
t2
)
if
t1
==
t2
=>
t1
case
And
(
t1
,
t2
)
if
t1
==
t2
=>
t1
case
Or
(
t1
,
t2
)
if
t1
==
t2
=>
t1
case
And
(
t1
,
And
(
t2
,
t3
))
if
(
t1
==
t2
)
=>
And
(
t1
,
t3
)
case
And
(
t1
,
And
(
t2
,
t3
))
if
(
t1
==
t3
)
=>
And
(
t1
,
t2
)
case
Or
(
t1
,
Or
(
t2
,
t3
))
if
(
t1
==
t2
)
=>
Or
(
t1
,
t3
)
case
Or
(
t1
,
Or
(
t2
,
t3
))
if
(
t1
==
t3
)
=>
Or
(
t1
,
t2
)
case
Or
(
t1
,
Or
(
t2
,
t3
))
if
(
t1
==
t2
)
=>
Or
(
t1
,
t3
)
case
Or
(
t1
,
Or
(
t2
,
t3
))
if
(
t1
==
t3
)
=>
Or
(
t1
,
t2
)
// And Or
case
And
(
t1
,
Or
(
t2
,
t3
))
if
(
t1
==
t3
)
=>
t1
case
And
(
t1
,
Or
(
t2
,
t3
))
if
(
t1
==
t2
)
=>
t1
case
And
(
Or
(
t2
,
t3
),
t1
)
if
(
t1
==
t3
)
=>
t1
case
And
(
Or
(
t2
,
t3
),
t1
)
if
(
t1
==
t2
)
=>
t1
case
And
(
t1
,
Or
(
t2
,
t3
))
if
(
t1
==
t3
)
=>
t1
case
And
(
t1
,
Or
(
t2
,
t3
))
if
(
t1
==
t2
)
=>
t1
case
And
(
Or
(
t2
,
t3
),
t1
)
if
(
t1
==
t3
)
=>
t1
case
And
(
Or
(
t2
,
t3
),
t1
)
if
(
t1
==
t2
)
=>
t1
// case Or(t1, Neg(t2)) if t1 == t2 => True
// Equivalence
case
Eq
(
t1
,
t2
)
if
t1
==
t2
=>
True
case
Eq
(
t1
,
t2
)
if
t1
==
t2
=>
True
// Double Temporals
case
Finally
(
Finally
(
t
))
=>
Finally
(
t
)
case
Globally
(
Globally
(
t
))
=>
Globally
(
t
)
case
Finally
(
Finally
(
t
))
=>
Finally
(
t
)
case
Globally
(
Globally
(
t
))
=>
Globally
(
t
)
// Remove quantifiers if empty
case
Quantifier
(
_
,
xs
,
t
)
if
xs
.
isEmpty
=>
t
case
Quantifier
(
_
,
_
,
True
)
=>
True
case
Quantifier
(
_
,
_
,
False
)
=>
False
case
Quantifier
(
_
,
_
,
True
)
=>
True
case
Quantifier
(
_
,
_
,
False
)
=>
False
// Quantifiers binding same things
case
And
(
Forall
(
vars1
,
t1
),
Forall
(
vars2
,
t2
))
if
(
vars1
==
vars2
)
=>
Forall
(
vars1
,
And
(
t1
,
t2
))
case
Or
(
Forall
(
vars1
,
t1
),
Forall
(
vars2
,
t2
))
if
(
vars1
==
vars2
)
=>
Forall
(
vars1
,
Or
(
t1
,
t2
))
...
...
@@ -99,8 +97,8 @@ object FormulaFunctions extends LazyLogging {
case
Or
(
Exists
(
vars1
,
t1
),
Exists
(
vars2
,
t2
))
if
(
vars1
==
vars2
)
=>
Exists
(
vars1
,
Or
(
t1
,
t2
))
// Gobble up equal quantifiers
case
Forall
(
vars1
,
Forall
(
vars2
,
f
))
=>
Forall
(
vars1
++
vars2
,
f
)
case
Exists
(
vars1
,
Exists
(
vars2
,
f
))
=>
Exists
(
vars1
++
vars2
,
f
)
case
Forall
(
vars1
,
Forall
(
vars2
,
f
))
=>
Forall
(
vars1
++
vars2
,
f
)
case
Exists
(
vars1
,
Exists
(
vars2
,
f
))
=>
Exists
(
vars1
++
vars2
,
f
)
// Remove variables from quantifiers if not used in the body: Caution - expensive
// case Quantifier(qmake, xs, t) if !(xs.toSet -- t.freeVars()).isEmpty =>
...
...
@@ -111,13 +109,43 @@ object FormulaFunctions extends LazyLogging {
// make(t1, qmake(xs, t2))
// case Quantifier(qmake, xs, BinOp(make, t1, t2)) if (t2.freeVars().intersect(xs.toSet)).isEmpty =>
// make(qmake(xs, t1), t2)
// Declass seen often enough
case
And
(
Or
(
f1
,
f2
),
Or
(
f3
,
f4
))
if
(
f2
==
f4
&&
f1
==
Neg
(
f3
).
simplify
())
=>
f2
}
// val (changed, t1) = everywhereFP(simp, t)
// if (!changed) t1 else simplify(t1)
// val (changed, t1) = everywhereFP(simp, t)
// if (!changed) t1 else simplify(t1)
everywhereBotUp
(
simp
,
t
)
}
def
pushQuantifiers
(
f
:
Formula
)
:
Formula
=
{
f
everywhere
{
case
Forall
(
vars
,
BinOp
(
make
,
f1
,
f2
))
if
{
val
leftvars
=
f1
.
freeVars
()
val
rightvars
=
f2
.
freeVars
()
val
varset
=
vars
.
toSet
val
onlyleft
=
leftvars
.
intersect
(
varset
)
--
rightvars
val
onlyright
=
rightvars
.
intersect
(
varset
)
--
leftvars
!
onlyleft
.
isEmpty
||
!
onlyright
.
isEmpty
}
=>
{
val
leftvars
=
f1
.
freeVars
()
val
rightvars
=
f2
.
freeVars
()
val
varset
=
vars
.
toSet
val
bothvars
=
leftvars
.
intersect
(
rightvars
).
intersect
(
varset
)
val
onlyleft
=
leftvars
.
intersect
(
varset
)
--
rightvars
val
onlyright
=
rightvars
.
intersect
(
varset
)
--
leftvars
Forall
.
make
(
bothvars
.
toList
,
make
(
pushQuantifiers
(
Forall
.
make
(
onlyleft
.
toList
,
f1
)),
pushQuantifiers
(
Forall
.
make
(
onlyright
.
toList
,
f2
))))
}
}
}
def
eliminateImplication
(
f
:
Formula
)
:
Formula
=
{
f
everywhere
{
case
Implies
(
f1
,
f2
)
=>
Or
(
Neg
(
eliminateImplication
(
f1
)),
eliminateImplication
(
f2
))
...
...
@@ -133,7 +161,7 @@ object FormulaFunctions extends LazyLogging {
}
}
}
def
everywhereFP
(
trans
:
PartialFunction
[
Formula
,
Formula
],
t
:
Formula
)
:
(
Boolean
,
Formula
)
=
{
if
(
trans
.
isDefinedAt
(
t
))
(
true
,
trans
(
t
))
...
...
@@ -144,16 +172,16 @@ object FormulaFunctions extends LazyLogging {
val
sub
=
everywhereFP
(
trans
,
t1
)
(
sub
.
_1
,
make
(
ps
,
sub
.
_2
))
}
case
UnOp
(
make
,
t1
)
=>
{
case
UnOp
(
make
,
t1
)
=>
{
val
sub
=
everywhereFP
(
trans
,
t1
)
(
sub
.
_1
,
make
(
sub
.
_2
))
}
case
BinOp
(
make
,
t1
,
t2
)
=>
{
case
BinOp
(
make
,
t1
,
t2
)
=>
{
val
(
c1
,
sub1
)
=
everywhereFP
(
trans
,
t1
)
val
(
c2
,
sub2
)
=
everywhereFP
(
trans
,
t2
)
(
c1
||
c2
,
make
(
sub1
,
sub2
))
}
case
x
=>
(
false
,
x
)
case
x
=>
(
false
,
x
)
}
}
...
...
@@ -169,7 +197,7 @@ object FormulaFunctions extends LazyLogging {
case
x
=>
x
}
}
def
everywhereBotUp
(
trans
:
PartialFunction
[
Formula
,
Formula
],
t
:
Formula
)
:
Formula
=
{
// First apply trans to push negation inward etc
if
(
trans
.
isDefinedAt
(
t
))
...
...
@@ -226,7 +254,7 @@ object FormulaFunctions extends LazyLogging {
}
}
def
hasSubFormula
(
coll
:
PartialFunction
[
Formula
,
Boolean
],
t
:
Formula
)
:
Boolean
=
{
def
hasSubFormula
(
coll
:
PartialFunction
[
Formula
,
Boolean
],
t
:
Formula
)
:
Boolean
=
{
def
or
(
bs
:
Boolean*
)
=
{
bs
.
exists
(
identity
)
}
collect
(
or
)(
coll
,
t
)
}
...
...
@@ -347,33 +375,31 @@ object FormulaFunctions extends LazyLogging {
// TODO: merge universals with same type by renaming
val
ex1
=
q1
.
takeWhile
(
_
.
_1
)
val
rest1
=
q1
.
drop
(
ex1
.
size
)
// filter out same bound variables (TODO: could be improved if different names)
val
existbound
=
ex1
.
flatMap
(
_
.
_2
)
val
univbound
=
rest1
.
flatMap
(
_
.
_2
)
val
exset
=
existbound
.
toSet
val
univset
=
univbound
.
toSet
val
ex2
=
q2
.
takeWhile
(
_
.
_1
).
map
(
q
=>
(
q
.
_1
,
q
.
_2
.
filterNot
(
exset
.
contains
))
)
(
q
.
_1
,
q
.
_2
.
filterNot
(
exset
.
contains
)))
val
rest2
=
q2
.
drop
(
ex2
.
size
).
map
(
q
=>
(
q
.
_1
,
q
.
_2
.
filterNot
(
univset
.
contains
))
)
(
q
.
_1
,
q
.
_2
.
filterNot
(
univset
.
contains
)))
ex1
++
ex2
++
rest1
++
rest2
}
}
}
def
checkBindings
(
f
:
Formula
)
=
{
def
checkBindingsSub
(
f
:
Formula
,
bound
:
Set
[
Var
])
:
List
[
Var
]
=
{
f
collect
{
case
Quantifier
(
make
,
xs
,
inner
)
=>
{
val
conflicts
=
xs
.
filter
(
bound
.
contains
)
conflicts
++
checkBindingsSub
(
inner
,
bound
++
xs
)
}
def
checkBindings
(
f
:
Formula
)
=
{
def
checkBindingsSub
(
f
:
Formula
,
bound
:
Set
[
Var
])
:
List
[
Var
]
=
{
f
collect
{
case
Quantifier
(
make
,
xs
,
inner
)
=>
{
val
conflicts
=
xs
.
filter
(
bound
.
contains
)
conflicts
++
checkBindingsSub
(
inner
,
bound
++
xs
)
}
}
}
checkBindingsSub
(
f
,
Set
()).
isEmpty
}
...
...
@@ -389,16 +415,15 @@ object FormulaFunctions extends LazyLogging {
def
isQFree
(
formula
:
Formula
)
:
Boolean
=
{
!
formula
.
hasSubFormula
{
case
q
:
Quantifier
=>
true
case
q
:
Quantifier
=>
true
}
}
def
toNegNf
(
f
:
Formula
)
=
{
// val bound = if (hasDuplicateBindings(f)) {
// // logger.info(s"Formula binds variables more than once - renaming bindings: ${f.pretty}")
// FormulaFunctions.fixBinding(f, Set())._1
// } else f
// val bound = if (hasDuplicateBindings(f)) {
// // logger.info(s"Formula binds variables more than once - renaming bindings: ${f.pretty}")
// FormulaFunctions.fixBinding(f, Set())._1
// } else f
val
noeq
=
eliminateEq
(
f
)
eliminateImplication
(
noeq
).
simplify
()
}
...
...
@@ -445,9 +470,9 @@ object FormulaFunctions extends LazyLogging {
}
// TODO: make sure no quantifiers in scope of others with same name
def
toPrenex
(
f
:
Formula
)
:
Formula
=
{
def
toPrenex
(
f
:
Formula
)
:
Formula
=
{
val
negnf
=
f
.
toNegNf
// val (simp, boundVars) = fixBinding(negnf, Set())
// val (simp, boundVars) = fixBinding(negnf, Set())
// Simplify first to push negation inward
val
quants
=
collectQuantifiers
(
negnf
)
...
...
@@ -480,25 +505,37 @@ object FormulaFunctions extends LazyLogging {
case
Or
(
And
(
f1
,
f2
),
f3
)
=>
And
(
Or
(
f1
,
f3
),
Or
(
f2
,
f3
))
case
Or
(
f1
,
And
(
f2
,
f3
))
=>
And
(
Or
(
f1
,
f2
),
Or
(
f1
,
f3
))
},
normalized
)
val
quantifiers
=
FormulaFunctions
.
collectQuantifiers
(
cnf1
)
// Inspect clauses
val
clauses
=
FOTransformers
.
collectClauses
(
cnf1
)
// TODO: improve, don't sort by tostring
val
sorted
=
clauses
.
map
(
c
=>
c
.
sortBy
(
_
.
toString
())).
sortBy
(
f
=>
f
.
toString
())
logger
.
debug
(
s
"Computing CNF of a formula with ${sorted.size} clauses"
)
// Remove trivial clauses
val
notrivials
=
sorted
.
filterNot
(
c
=>
{
c
.
exists
(
f
=>
c
.
contains
(
Neg
(
f
)))
})
// TODO improve runtime
val
simpedset
=
clauses
.
toSet
val
simped
=
simpedset
.
filterNot
(
c
=>
simpedset
.
exists
(
c2
=>
{
val
simped
=
notrivials
.
filterNot
(
c
=>
notrivials
.
exists
(
c2
=>
{
// check if c is superset of c2
c
!=
c2
&&
c
.
startsWith
(
c2
)
// c != c2 && c.startsWith(c2)
c
!=
c2
&&
c
.
forall
(
f
=>
c2
.
contains
(
f
))
}))
(
quantifiers
,
clauses
)
logger
.
debug
(
s
"After simplification ${simped.size} unsubsumed clauses remaining."
)
(
quantifiers
,
simped
)
}
def
toCNF
(
f
:
Formula
)
=
{
val
(
quantifiers
,
clauses
)
=
toCNFClauses
(
f
)
def
toCNF
(
f
:
Formula
)
=
{
val
(
quantifiers
,
clauses
)
=
toCNFClauses
(
f
)
val
form
=
And
.
make
(
clauses
.
map
(
Or
.
make
))
val
newform
=
quantifiers
.
foldRight
(
form
)((
q
,
inner
)
=>
if
(
q
.
_1
)
Exists
(
q
.
_2
,
inner
)
else
Forall
(
q
.
_2
,
inner
))
val
newform
=
quantifiers
.
foldRight
(
form
)((
q
,
inner
)
=>
if
(
q
.
_1
)
Exists
(
q
.
_2
,
inner
)
else
Forall
(
q
.
_2
,
inner
))
newform
}
...
...
src/main/scala/de/tum/workflows/toz3/InvariantGenerator.scala
View file @
0f390288
...
...
@@ -42,6 +42,8 @@ object InvariantGenerator {
val
conclusion
=
genEq
(
spec
.
target
,
spec
.
target
.
params
)
Forall
(
spec
.
target
.
params
,
conclusion
).
simplify
()
// Constants
// conclusion
}
// def invariantNoninterStubbornBS(spec: Spec) = {
...
...
src/main/scala/de/tum/workflows/toz3/Z3QFree.scala
View file @
0f390288
...
...
@@ -10,7 +10,6 @@ import com.typesafe.scalalogging.LazyLogging
import
de.tum.workflows.Utils
import
de.tum.workflows.foltl.FOTransformers
import
de.tum.workflows.foltl.FormulaFunctions
import
it.unimi.dsi.fastutil.longs.Long2BooleanArrayMap
object
Z3QFree
extends
LazyLogging
{
...
...
src/test/scala/de/tum/workflows/tests/FOLTLTest.scala
View file @
0f390288
...
...
@@ -6,6 +6,7 @@ import org.scalatest.Inspectors._
import
de.tum.workflows.foltl.FOLTL._
import
de.tum.workflows.Implicits._
import
de.tum.workflows.foltl.FOLTL
import
de.tum.workflows.foltl.FormulaFunctions
class
FOLTLTest
extends
FlatSpec
{
"Formulas"
should
"be constructed correctly"
in
{
...
...
@@ -150,4 +151,20 @@ class FOLTLTest extends FlatSpec {
))
)
}
it
should
"not fail at doing so"
in
{
val
f
=
Forall
(
List
(
"xt"
,
"pt"
,
"yt"
,
"p"
),
And
.
make
(
Neg
(
Fun
(
"B"
,
List
(
"xt"
,
"pt"
))),
Neg
(
Fun
(
"B"
,
List
(
"yt"
,
"p"
))),
Neg
(
Fun
(
"B"
,
List
(
"yt"
,
"pt"
))),
Neg
(
Fun
(
"Conf"
,
Some
(
"t1"
),
List
(
"xt"
,
"p"
)))
))
f
.
toCNF
should
be
(
f
)