Skip to content
Projects
Groups
Snippets
Help
Loading...
Help
Support
Keyboard shortcuts
?
Submit feedback
Contribute to GitLab
Sign in
Toggle navigation
N
NIWO
Project overview
Project overview
Details
Activity
Releases
Repository
Repository
Files
Commits
Branches
Tags
Contributors
Graph
Compare
Issues
0
Issues
0
List
Boards
Labels
Milestones
Merge Requests
0
Merge Requests
0
CI / CD
CI / CD
Pipelines
Jobs
Schedules
Packages
Packages
Container Registry
Analytics
Analytics
CI / CD
Repository
Value Stream
Wiki
Wiki
Members
Members
Collapse sidebar
Close sidebar
Activity
Graph
Create a new issue
Jobs
Commits
Issue Boards
Open sidebar
Christian Müller
NIWO
Commits
0a3d0c62
Commit
0a3d0c62
authored
Feb 25, 2019
by
Christian Müller
Browse files
Options
Browse Files
Download
Email Patches
Plain Diff
inference fixes all about
parent
48fb7dd3
Changes
15
Hide whitespace changes
Inline
Side-by-side
Showing
15 changed files
with
176 additions
and
113 deletions
+176
-113
examples/tests/conference_linear_small_withB.spec
examples/tests/conference_linear_small_withB.spec
+4
-4
src/main/scala/de/tum/workflows/Encoding.scala
src/main/scala/de/tum/workflows/Encoding.scala
+8
-4
src/main/scala/de/tum/workflows/Preconditions.scala
src/main/scala/de/tum/workflows/Preconditions.scala
+36
-14
src/main/scala/de/tum/workflows/WorkflowParser.scala
src/main/scala/de/tum/workflows/WorkflowParser.scala
+5
-3
src/main/scala/de/tum/workflows/blocks/Workflow.scala
src/main/scala/de/tum/workflows/blocks/Workflow.scala
+12
-3
src/main/scala/de/tum/workflows/foltl/FOLTL.scala
src/main/scala/de/tum/workflows/foltl/FOLTL.scala
+9
-5
src/main/scala/de/tum/workflows/foltl/FOTransformers.scala
src/main/scala/de/tum/workflows/foltl/FOTransformers.scala
+36
-26
src/main/scala/de/tum/workflows/foltl/FormulaFunctions.scala
src/main/scala/de/tum/workflows/foltl/FormulaFunctions.scala
+4
-5
src/main/scala/de/tum/workflows/toz3/InvariantChecker.scala
src/main/scala/de/tum/workflows/toz3/InvariantChecker.scala
+10
-30
src/test/scala/de/tum/workflows/tests/InferenceTests.scala
src/test/scala/de/tum/workflows/tests/InferenceTests.scala
+33
-0
src/test/scala/de/tum/workflows/tests/InvariantSmallCausalFiltesTest.scala
.../tum/workflows/tests/InvariantSmallCausalFiltesTest.scala
+5
-5
src/test/scala/de/tum/workflows/tests/TestUtils.scala
src/test/scala/de/tum/workflows/tests/TestUtils.scala
+6
-6
src/test/scala/de/tum/workflows/tests/papertests/DemoNoStrengtheningTests.scala
...workflows/tests/papertests/DemoNoStrengtheningTests.scala
+2
-2
src/test/scala/de/tum/workflows/tests/papertests/DemoUniversity.scala
...la/de/tum/workflows/tests/papertests/DemoUniversity.scala
+1
-1
src/test/scala/de/tum/workflows/tests/papertests/InvariantCausalFilesTest.scala
...workflows/tests/papertests/InvariantCausalFilesTest.scala
+5
-5
No files found.
examples/tests/conference_linear_small_withB.spec
View file @
0a3d0c62
...
...
@@ -4,14 +4,14 @@ forallmay x:X,p:P
True -> Conf += (x,p)
forall x:x,p:P
B(x,p) -> Assign += (x,p)
forall x:X,p:P
,r:R
(Assign(x,p) ∧ O(x,p
,r)) -> Read += (x,p,r
)
forall x:X,p:P
(Assign(x,p) ∧ O(x,p
)) -> Report += (x,p
)
forallmay y:X,x:X,p:P
(
Assign
(x,p) ∧ Assign(y,p)) -> Comm += (x,y,p)
(
Report
(x,p) ∧ Assign(y,p)) -> Comm += (x,y,p)
Declassify
O(x:X,p:P
,r:R
): ¬ Conf(xt:X,p:P)
O(x:X,p:P): ¬ Conf(xt:X,p:P)
Target
...
...
src/main/scala/de/tum/workflows/Encoding.scala
View file @
0a3d0c62
...
...
@@ -6,7 +6,7 @@ import scalax.collection.GraphEdge._
import
scalax.collection.edge.LDiEdge
import
scalax.collection.edge.Implicits._
import
blocks._
import
de.tum.workflows.foltl.
FOLTL
import
de.tum.workflows.foltl.
{
FOLTL
,
Properties
}
import
de.tum.workflows.foltl.FOLTL._
import
de.tum.workflows.foltl.FormulaFunctions._
import
com.typesafe.scalalogging._
...
...
@@ -253,7 +253,7 @@ object Encoding extends LazyLogging {
*
* @param w the graph
*/
def
untouchedMap
(
g
:
WorkflowGraph
,
sig
:
Signature
)
:
Map
[
g.NodeT
,
Set
[
String
]]
=
{
def
untouchedMap
(
g
:
WorkflowGraph
,
sig
:
Signature
,
props
:
InvProperties
)
:
Map
[
g.NodeT
,
Set
[
String
]]
=
{
val
sourceid
=
0
val
sourcenode
=
g
.
get
(
sourceid
)
...
...
@@ -274,7 +274,11 @@ object Encoding extends LazyLogging {
}
}
map
// For causal agents add informedness - only at the end to not propagate it (as its not mentioned in the graph)
if
(!
props
.
stubborn
)
{
map
.
updated
(
sourcenode
,
map
(
sourcenode
)
+
Properties
.
INFNAME
)
}
else
{
map
}
}
}
\ No newline at end of file
src/main/scala/de/tum/workflows/Preconditions.scala
View file @
0a3d0c62
...
...
@@ -2,10 +2,10 @@ package de.tum.workflows
import
com.typesafe.scalalogging._
import
blocks._
import
de.tum.workflows.foltl.
{
FOLTL
,
FOTransformers
,
FormulaFunctions
}
import
de.tum.workflows.foltl.
{
FOLTL
,
FOTransformers
,
FormulaFunctions
,
Properties
}
import
de.tum.workflows.foltl.FOLTL._
import
de.tum.workflows.foltl.Properties._
import
de.tum.workflows.toz3.
InvProperties
import
de.tum.workflows.toz3.
{
InvProperties
,
Z3BSFO
}
object
Preconditions
extends
LazyLogging
{
...
...
@@ -98,7 +98,8 @@ object Preconditions extends LazyLogging {
val
guard
=
And
(
s
.
guard
,
con
).
simplify
// val guard = True
val
frees
=
guard
.
freeVars
--
s
.
tuple
.
toSet
val
frees
=
guard
.
freeVars
--
s
.
tuple
.
toSet
--
spec
.
constants
val
form
=
s
match
{
case
Add
(
_
,
_
,
_
)
=>
{
...
...
@@ -144,38 +145,59 @@ object Preconditions extends LazyLogging {
// TODO: have we proven this correct?
val
removed
=
FOTransformers
.
eliminateDoubleQuantifiers
(
replaced
)
if
(
Utils
.
DEBUG_MODE
)
{
if
(
FormulaFunctions
.
collectQuantifiers
(
removed
)
!=
FormulaFunctions
.
collectQuantifiers
(
replaced
))
{
logger
.
warn
(
s
"Removed a quantifier:\nBefore: $replaced\nAfter:$removed"
)
}
}
removed
}
def
abstractedPrecondition
(
f
:
Formula
,
b
:
SimpleBlock
,
s
:
Spec
,
properties
:
InvProperties
)
=
{
def
abstractedPrecondition
(
f
:
Formula
,
b
:
SimpleBlock
,
s
:
Spec
,
properties
:
InvProperties
,
untouched
:
Set
[
String
]
)
=
{
val
precond
=
weakestPrecondition
(
f
,
b
,
s
,
properties
)
// Abstract away inner existentials - always if causal agents
val
universalinv
=
if
(!
properties
.
stubborn
||
b
.
isomitting
)
{
FOTransformers
.
abstractExistentials
(
precond
)
// Assume untoucheds empty
val
untouchedprecond
=
precond
.
assumeEmpty
(
untouched
.
toList
)
val
z3simpednewinv
=
Z3BSFO
.
simplifyBS
(
untouchedprecond
)
// Abstract away inner existentials
val
universalinv
=
if
(
z3simpednewinv
.
toNegNf
.
hasSubFormula
{
case
e
:
Exists
=>
true
})
{
FOTransformers
.
abstractExistentials
(
z3simpednewinv
)
}
else
{
precond
z3simpednewinv
}
//
Abstract away auxilliari
es
//
Eliminate Choic
es
val
auxless
=
if
(
b
.
pred
.
isDefined
&&
properties
.
eliminateAux
)
{
FOTransformers
.
eliminateAuxiliaryPredicate
(
universalinv
,
b
.
pred
.
get
)
}
else
{
universalinv
}
// Eliminate Oracles
val
oless
=
if
(
properties
.
eliminateAux
)
{
val
oracles
=
auxless
.
collect
{
case
f
:
Fun
if
f.isOracle
()
=>
List
(
f
.
name
)
}.
toSet
oracles
.
foldRight
(
auxless
)((
b
,
inv
)
=>
FOTransformers
.
eliminateAuxiliaryPredicate
(
inv
,
b
))
}
else
{
auxless
}
// Win game
val
bless
=
if
(
properties
.
eliminateB
)
{
val
bs
=
aux
less
.
collect
{
val
bs
=
o
less
.
collect
{
case
f
:
Fun
if
f.isB
()
=>
List
(
f
.
name
)
}.
toSet
val
eliminv
=
bs
.
foldRight
(
auxless
)((
b
,
inv
)
=>
FOTransformers
.
eliminateBPredicate
(
inv
,
b
).
_1
)
eliminv
bs
.
foldRight
(
oless
)((
b
,
inv
)
=>
FOTransformers
.
eliminateBPredicate
(
inv
,
b
).
_1
)
}
else
{
aux
less
o
less
}
bless
.
simplify
Z3BSFO
.
simplifyBS
(
bless
.
simplify
)
}
}
\ No newline at end of file
src/main/scala/de/tum/workflows/WorkflowParser.scala
View file @
0a3d0c62
...
...
@@ -76,9 +76,11 @@ object WorkflowParser extends RegexParsers with PackratParsers with LazyLogging
val
preds
=
allpredicates
(
list
)
// Filter to just the first
val
filtered
=
preds
groupBy
(
_
.
name
)
map
(
_
.
_2
.
head
)
val
(
oracles
,
rels
)
=
filtered
.
partition
(
_
.
name
.
startsWith
(
"O"
))
Signature
(
oracles
toSet
,
rels
toSet
)
val
filtered
=
preds
groupBy
(
_
.
name
)
map
(
_
.
_2
.
head
)
toSet
val
oracles
=
filtered
.
filter
(
_
.
isOracle
())
val
bs
=
filtered
.
filter
(
_
.
isB
())
val
rels
=
filtered
--
oracles
--
bs
Signature
(
oracles
,
rels
)
}
def
typeMap
(
typedvars
:
List
[
Var
])
=
{
...
...
src/main/scala/de/tum/workflows/blocks/Workflow.scala
View file @
0a3d0c62
...
...
@@ -23,6 +23,15 @@ case class Spec(w: Workflow, declass: Map[String, (List[Var], Formula)], target:
override
def
toString
=
{
s
"Spec\nWorkflow:\n$w\nDeclass:$declass\nTarget:$target"
}
lazy
val
constants
:
Set
[
Var
]
=
{
// Treat free variables in the declassification as constants
declass
.
values
.
flatMap
{
case
(
params
,
f
)
=>
f
.
freeVars
--
params
}.
toSet
// TODO: How to check for more constants?
}
def
checkSanity
()
=
{
var
sane
=
true
...
...
@@ -33,7 +42,7 @@ case class Spec(w: Workflow, declass: Map[String, (List[Var], Formula)], target:
val
ta
=
target
.
params
.
head
// check declass bindings
for
((
o
,
(
f
,
t
))
<-
declass
if
!
t
.
freeVars
.
forall
(
v
=>
(
f
.
contains
(
v
)
||
(
v
==
ta
)
)))
{
for
((
o
,
(
f
,
t
))
<-
declass
if
!
t
.
freeVars
.
forall
(
v
=>
f
.
contains
(
v
)
||
(
v
==
ta
)))
{
logger
.
error
(
s
"Not all variables of the declassification condition for $o bound by the oracle"
)
sane
=
false
}
...
...
@@ -41,9 +50,9 @@ case class Spec(w: Workflow, declass: Map[String, (List[Var], Formula)], target:
def
saneoraclestmt
(
stmt
:
Statement
,
frees
:
List
[
Var
])
=
{
// Oracle only positive
val
f
=
stmt
.
guard
.
toNegNf
val
noneg
=
!
(
f
.
hasSubFormula
{
val
noneg
=
!
f
.
hasSubFormula
{
case
Neg
(
f
:
Fun
)
if
f
.
isOracle
()
=>
true
}
)
}
val
allvars
=
!(
f
hasSubFormula
{
case
f
:
Fun
if
f.isOracle
&&
f.params
!=
frees
=>
true
})
...
...
src/main/scala/de/tum/workflows/foltl/FOLTL.scala
View file @
0a3d0c62
...
...
@@ -259,14 +259,18 @@ object FOLTL {
// case List() => acc
// }
// }
def
makeL
(
make
:
(
Formula
,
Formula
)
=>
Formula
,
l
:
Seq
[
Formula
],
Empty
:
Formula
)
:
Formula
=
{
l
.
toList
match
{
def
makeL
(
make
:
(
Formula
,
Formula
)
=>
Formula
,
l
:
Seq
[
Formula
],
Empty
:
Formula
)
:
Formula
=
{
def
inner
(
l
:
List
[
Formula
])
:
Formula
=
{
l
match
{
case
List
(
x
)
=>
x
case
Empty
::
xs
=>
makeL
(
make
,
xs
,
Empty
)
case
x
::
xs
=>
make
(
x
,
makeL
(
make
,
xs
,
Empty
))
case
Empty
::
xs
=>
inner
(
xs
)
case
x
::
xs
=>
make
(
x
,
inner
(
xs
))
case
List
()
=>
Empty
}
}
}
// Filter unique
inner
(
l
.
toList
.
distinct
)
}
}
object
Or
{
...
...
src/main/scala/de/tum/workflows/foltl/FOTransformers.scala
View file @
0a3d0c62
...
...
@@ -55,7 +55,7 @@ object FOTransformers extends LazyLogging {
}
def
eliminateAuxiliaryPredicate
(
f
:
Formula
,
AUX
:
String
)
=
{
logger
.
info
(
s
"Eliminating universal second order predicate $AUX"
)
logger
.
debug
(
s
"Eliminating universal second order predicate $AUX"
)
val
cnf
=
f
.
toCNF
...
...
@@ -70,12 +70,13 @@ object FOTransformers extends LazyLogging {
// TODO: What to do with B(T1) and B(T2) instead of this?
def
eliminateBPredicate
(
f
:
Formula
,
B
:
String
)
=
{
// SOQE: \exists B. f <-> f'
logger
.
info
(
s
"Eliminating existential second order predicate $B"
)
logger
.
debug
(
s
"Eliminating existential second order predicate $B"
)
if
(!
f
.
isUniversal
)
{
logger
.
error
(
"Trying to use SOQE on a non-universal formula"
)
}
// This sets B(T1) and B(T2) to be the same relation
// Use the best available simplification
val
noannotation
=
Z3BSFO
.
simplifyBS
(
FormulaFunctions
.
removeAnnotation
(
f
,
B
))
val
(
quantifiers
,
clauses
)
=
FormulaFunctions
.
toCNFClauses
(
noannotation
)
...
...
@@ -88,79 +89,88 @@ object FOTransformers extends LazyLogging {
getNegativeBArguments
(
clause
).
nonEmpty
def
pruneBs
(
clause
:
List
[
Formula
])
=
{
clause
.
filterNot
{
clause
filterNot
{
case
Neg
(
Fun
(
B
,
_
,
_
))
=>
true
case
Fun
(
B
,
_
,
_
)
=>
true
case
_
=>
false
}
}
def
getPositiveBArguments
(
clause
:
List
[
Formula
])
:
Lis
t
[
List
[
Var
]]
=
{
def
getPositiveBArguments
(
clause
:
List
[
Formula
])
:
Se
t
[
List
[
Var
]]
=
{
clause
flatMap
{
case
Fun
(
B
,
_
,
vars
)
=>
List
(
vars
)
case
_
=>
List
()
}
}
toSet
}
def
getNegativeBArguments
(
clause
:
List
[
Formula
])
:
Lis
t
[
List
[
Var
]]
=
{
def
getNegativeBArguments
(
clause
:
List
[
Formula
])
:
Se
t
[
List
[
Var
]]
=
{
clause
flatMap
{
case
Neg
(
Fun
(
B
,
_
,
vars
))
=>
List
(
vars
)
case
_
=>
List
()
}
}
toSet
}
def
ineq
(
l1
:
List
[
Var
],
l2
:
List
[
Var
])
=
{
if
(
l1
.
size
!=
l2
.
size
)
{
logger
.
warn
(
"Trying to generate inequalities for different sized vectors"
)
}
Or
.
make
(
l1
.
zip
(
l2
).
map
{
case
(
x
,
y
)
=>
Neg
(
Eq
(
x
,
y
))
})
val
ineqs
=
l1
.
zip
(
l2
).
filterNot
(
x
=>
x
.
_1
==
x
.
_2
).
map
{
case
(
x
,
y
)
if
x
.
name
<=
y
.
name
=>
Neg
(
Eq
(
x
,
y
))
case
(
x
,
y
)
=>
Neg
(
Eq
(
y
,
x
))
}.
toSet
Or
.
make
(
ineqs
.
toList
)
}
val
E
=
clauses
.
filter
(
c
=>
!
ispositive
(
c
)
&&
!
isnegative
(
c
))
val
F
=
clauses
.
filter
(
c
=>
ispositive
(
c
)
&&
!
isnegative
(
c
))
// F \/ B z_1 ... B z_r
val
Fargs
=
F
.
flatM
ap
(
getPositiveBArguments
)
val
Fargs
=
F
.
m
ap
(
getPositiveBArguments
)
val
G
=
clauses
.
filter
(
c
=>
isnegative
(
c
)
&&
!
ispositive
(
c
))
// G \/ !B z'_1 ... !B z'_j
val
Gargs
=
G
.
flatM
ap
(
getNegativeBArguments
)
val
Gargs
=
G
.
m
ap
(
getNegativeBArguments
)
val
H
=
clauses
.
filter
(
c
=>
ispositive
(
c
)
&&
isnegative
(
c
))
// H \/ B u_1 .. B u_l \/ !B v_1 ... ! B v_n
val
HPositiveargs
=
H
.
flatM
ap
(
getPositiveBArguments
)
val
HNegativeargs
=
H
.
flatM
ap
(
getNegativeBArguments
)
val
HPositiveargs
=
H
.
m
ap
(
getPositiveBArguments
)
val
HNegativeargs
=
H
.
m
ap
(
getNegativeBArguments
)
if
(
H
.
nonEmpty
)
{
logger
.
warn
(
"BSFO SOQE: H is not empty, Ackermann not applicable"
)
}
val
fE
=
And
.
make
(
E
.
map
(
c
=>
Or
.
make
(
pruneBs
(
c
))))
val
f
F
=
And
.
make
(
F
.
map
(
c
=>
Or
.
make
(
pruneBs
(
c
)
)))
val
fG
=
And
.
make
(
G
.
map
(
c
=>
Or
.
make
(
pruneBs
(
c
)
)))
val
fH
=
And
.
make
(
G
.
map
(
c
=>
Or
.
make
(
pruneBs
(
c
)
)))
val
f
is
=
F
.
map
(
c
=>
Or
.
make
(
pruneBs
(
c
)))
val
gks
=
G
.
map
(
c
=>
Or
.
make
(
pruneBs
(
c
)))
val
hls
=
H
.
map
(
c
=>
Or
.
make
(
pruneBs
(
c
)))
val
fFGineq
=
And
.
make
(
for
(
farg
<-
Fargs
;
garg
<-
Gargs
)
yield
{
ineq
(
farg
,
garg
)
})
val
fGHineq
=
And
.
make
(
for
(
harg
<-
HPositiveargs
;
garg
<-
Gargs
)
yield
{
ineq
(
harg
,
garg
)
})
val
FGineq
=
for
((
fi
,
fargs
)
<-
fis
.
zip
(
Fargs
);
(
gk
,
gargs
)
<-
gks
.
zip
(
Gargs
);
farg
<-
gargs
;
garg
<-
gargs
)
yield
{
Or
.
make
(
fi
,
gk
,
ineq
(
farg
,
garg
))
}
val
fFGineq
=
And
.
make
(
FGineq
)
val
simpfFGineq
=
Z3BSFO
.
simplifyBS
(
fFGineq
)
// FIXME: is this correct? there are no quantifiers binding stuff
val
felim
:
Formula
=
fE
land
(
fF
lor
fG
lor
fFGineq
)
land
(
fH
lor
fGHineq
lor
fG
)
val
GHineq
=
for
((
hl
,
hargs
)
<-
hls
.
zip
(
HPositiveargs
);
(
gk
,
gargs
)
<-
gks
.
zip
(
Gargs
);
harg
<-
hargs
;
garg
<-
gargs
)
yield
{
Or
.
make
(
hl
,
gk
,
ineq
(
harg
,
garg
))
}
val
fGHineq
=
And
.
make
(
FGineq
)
val
simpfGHineq
=
Z3BSFO
.
simplifyBS
(
fGHineq
)
val
felim
:
Formula
=
fE
land
fFGineq
land
fGHineq
// TODO: Add ineq with ys
val
fsol
:
Formula
=
fG
val
fsol
:
Formula
=
And
.
make
(
gks
)
// wrap quantifiers around
val
felimq
=
FormulaFunctions
.
rewrapQuantifiers
(
quantifiers
,
felim
)
val
fsolq
=
FormulaFunctions
.
rewrapQuantifiers
(
quantifiers
,
fsol
)
val
z3fsolq
=
Z3BSFO
.
simplifyBS
(
fsolq
)
if
(
Utils
.
DEBUG_MODE
)
{
logger
.
info
(
s
"BSFO SOQE: strategy for $B: $z3fsolq"
)
}
(
Z3BSFO
.
simplifyBS
(
felimq
)
,
z3fsolq
)
(
felimq
,
z3fsolq
)
}
/**
...
...
src/main/scala/de/tum/workflows/foltl/FormulaFunctions.scala
View file @
0a3d0c62
...
...
@@ -82,6 +82,7 @@ object FormulaFunctions extends LazyLogging {
// Equivalence
case
Eq
(
t1
,
t2
)
if
t1
==
t2
=>
True
case
Eq
(
v1
:
Var
,
v2
:
Var
)
if
v1
.
name
>
v2
.
name
=>
Eq
(
v2
,
v1
)
// Double Temporals
case
Finally
(
Finally
(
t
))
=>
Finally
(
t
)
...
...
@@ -584,7 +585,7 @@ object FormulaFunctions extends LazyLogging {
// if (f.isUniversal) {
// Z3BSFO.toCNFClausesUniversal(f)
// } else {
logger
.
warn
(
"Using internal CNF conversion - may blow up"
)
//
logger.warn("Using internal CNF conversion - may blow up")
// FIXME: can we do it without prenex? may be expensive later on
val
normalized
=
f
.
toPrenex
.
simplify
...
...
@@ -607,8 +608,6 @@ object FormulaFunctions extends LazyLogging {
// 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
)))
...
...
@@ -620,8 +619,8 @@ object FormulaFunctions extends LazyLogging {
// c != c2 && c.startsWith(c2)
c
!=
c2
&&
c
.
forall
(
f
=>
c2
.
contains
(
f
))
}))
logger
.
debug
(
s
"After simplification ${simped.size} unsubsumed clauses remaining."
)
//
logger.debug(s"After simplification ${simped.size} unsubsumed clauses remaining.")
logger
.
debug
(
s
"Resulting CNF has ${sorted.size} clauses"
)
(
quantifiers
,
simped
)
// }
}
...
...
src/main/scala/de/tum/workflows/toz3/InvariantChecker.scala
View file @
0a3d0c62
...
...
@@ -20,31 +20,14 @@ object InvProperties {
object
InvariantChecker
extends
LazyLogging
{
def
checkBlockInvariant
(
spec
:
Spec
,
b
:
SimpleBlock
,
pre
:
Formula
,
post
:
Formula
,
isfirst
:
Boolean
,
properties
:
InvProperties
,
untouched
:
Set
[
String
])
=
{
val
precond
=
Preconditions
.
abstractedPrecondition
(
post
,
b
,
spec
,
properties
)
// Assume untoucheds empty
val
untouchedprecond
=
precond
.
assumeEmpty
(
untouched
.
toList
)
// val firstprecond = if (isfirst) {
// precond.assumeEmpty(spec.w.sig.preds.map(_.name).toList)
// } else { precond }
val
noinfprecond
=
if
(
isfirst
&&
!
properties
.
stubborn
)
{
untouchedprecond
.
assumeEmpty
(
List
(
Properties
.
INFNAME
))
}
else
{
untouchedprecond
}
val
z3simpednewinv
=
Z3BSFO
.
simplifyBS
(
noinfprecond
)
val
gained
=
noinfprecond
.
toString
().
length
()
-
z3simpednewinv
.
toString
().
length
()
logger
.
info
(
s
"Invariant shrunken by $gained chars"
)
def
checkBlockInvariant
(
spec
:
Spec
,
b
:
SimpleBlock
,
pre
:
Formula
,
post
:
Formula
,
properties
:
InvProperties
,
untouched
:
Set
[
String
])
=
{
val
precond
=
Preconditions
.
abstractedPrecondition
(
post
,
b
,
spec
,
properties
,
untouched
)
// val test1 = inv.toPrenex()
// val test2 = stubprecond.toPrenex()
val
f
=
Implies
(
pre
,
z3simpednewinv
)
val
f
=
Implies
(
pre
,
precond
)
logger
.
info
(
s
"Checking invariant implication for $b"
)
(
Z3BSFO
.
checkAE
(
f
.
simplify
),
z3simpednewinv
)
(
Z3BSFO
.
checkAE
(
f
.
simplify
),
precond
)
}
def
checkInvariantFPLabelling
(
spec
:
Spec
,
inv
:
Formula
,
properties
:
InvProperties
)
=
{
...
...
@@ -52,7 +35,7 @@ object InvariantChecker extends LazyLogging {
type
Node
=
graph
.
NodeT
type
Edge
=
graph
.
EdgeT
val
untouched
=
Encoding
.
untouchedMap
(
graph
,
spec
.
w
.
sig
)
val
untouched
=
Encoding
.
untouchedMap
(
graph
,
spec
.
w
.
sig
,
properties
)
@tailrec
def
checkInvariantRec
(
labellist
:
List
[
Map
[
Int
,
Formula
]],
provenlist
:
List
[
Set
[
Edge
]])
:
(
Boolean
,
List
[
Map
[
Int
,
Formula
]],
List
[
Set
[
Edge
]])
=
{
...
...
@@ -76,8 +59,7 @@ object InvariantChecker extends LazyLogging {
// try to prove
val
pre
=
labels
(
nextEdge
.
from
)
val
post
=
labels
(
nextEdge
.
to
)
val
isfirst
=
!
nextEdge
.
from
.
hasPredecessors
val
((
status
,
solver
),
strengthened
)
=
checkBlockInvariant
(
spec
,
nextEdge
,
pre
,
post
,
isfirst
,
properties
,
untouched
(
nextEdge
.
from
))
val
((
status
,
solver
),
strengthened
)
=
checkBlockInvariant
(
spec
,
nextEdge
,
pre
,
post
,
properties
,
untouched
(
nextEdge
.
from
))
if
(
status
==
Status
.
UNSATISFIABLE
)
{
// Negation of implication unsat
...
...
@@ -101,6 +83,7 @@ object InvariantChecker extends LazyLogging {
val
newlabels
=
labels
.
updated
(
nextEdge
.
_1
,
newinv
)
val
isfirst
=
!
nextEdge
.
from
.
hasPredecessors
if
(!
isfirst
)
{
val
invalidated
=
proven
.
filter
(
_
.
to
==
nextEdge
.
from
)
val
newproven
=
(
proven
--
invalidated
)
+
nextEdge
...
...
@@ -126,7 +109,7 @@ object InvariantChecker extends LazyLogging {
// create labelling
val
labels
=
(
for
(
n
<-
graph
.
nodes
)
yield
{
n
.
value
->
inv
}).
toMap
// update labels with untouched map
// update
initial
labels with untouched map
val
untouchedlabels
=
for
((
n
,
inv
)
<-
labels
)
yield
{
n
->
inv
.
assumeEmpty
(
untouched
(
graph
.
get
(
n
)).
toList
)
}
...
...
@@ -155,7 +138,7 @@ object InvariantChecker extends LazyLogging {
// Build graph
val
graph
=
Encoding
.
toGraph
(
spec
.
w
)
val
untouched
=
Encoding
.
untouchedMap
(
graph
,
spec
.
w
.
sig
)
val
untouched
=
Encoding
.
untouchedMap
(
graph
,
spec
.
w
.
sig
,
properties
)
val
msg
=
new
StringBuilder
()
msg
++=
s
"Trying to prove safe with invariant:\n\n${inv.pretty}\n\n"
...
...
@@ -166,10 +149,7 @@ object InvariantChecker extends LazyLogging {
// Check I -> WP[w](inv)
val
b
:
SimpleBlock
=
e
// Special handling for first block
val
isfirst
=
!
e
.
from
.
hasPredecessors
val
((
res
,
solver
),
strengthened
)
=
checkBlockInvariant
(
spec
,
b
,
inv
,
inv
,
isfirst
,
properties
,
untouched
(
e
.
from
))
val
((
res
,
solver
),
strengthened
)
=
checkBlockInvariant
(
spec
,
b
,
inv
,
inv
,
properties
,
untouched
(
e
.
from
))
if
(
res
!=
Status
.
UNSATISFIABLE
)
{
msg
++=
s
"Possibly unsafe: Block may not uphold invariant:\n\n${e.label}\n\n"
...
...
src/test/scala/de/tum/workflows/tests/InferenceTests.scala
0 → 100644
View file @
0a3d0c62
package
de.tum.workflows.tests
import
org.scalatest.FlatSpec
import
org.scalatest.FlatSpec
import
org.scalatest.Matchers._
import
org.scalatest.Inspectors._
import
de.tum.workflows.foltl.FOLTL._
import
de.tum.workflows.Implicits._
import
de.tum.workflows.blocks._
import
de.tum.workflows.Preconditions
import
de.tum.workflows.foltl.FormulaFunctions
import
de.tum.workflows.ExampleWorkflows
import
de.tum.workflows.toz3.
{
InvariantChecker
,
InvariantGenerator
}
import
de.tum.workflows.Encoding._
import
de.tum.workflows.Utils
import
de.tum.workflows.Encoding
import
de.tum.workflows.tests.TestUtils._
import
de.tum.workflows.foltl.Properties
class
InferenceTests
extends
FlatSpec
{
"Invariant Inference"
should
"prove safe stuff safe"
in
{
val
name
=
"tests/conference_linear_small_withB"
val
xt
=
Var
(
"xt"
,
"X"
)
val
yt
=
Var
(
"yt"
,
"X"
)
val
pt
=
Var
(
"pt"
,
"P"
)
// val rt = Var("rt","R")
val
inv
=
Forall
(
List
(
pt
,
yt
),
genEq
(
"Comm"
,
List
(
xt
,
yt
,
pt
)))
assert
(
checkSafeStubborn
(
name
,
inv
))
}
}
src/test/scala/de/tum/workflows/tests/InvariantSmallCausalFiltesTest.scala
View file @
0a3d0c62
...
...
@@ -23,13 +23,13 @@ class InvariantSmallCausalFilesTest extends FlatSpec {
"InvariantChecker"
should
"prove simple causal may things safe"
in
{
val
name
=
"tests/simpleChoiceOmittingNoOracle"
val
inv
=
Forall
(
List
(
"xt"
),
genEq
(
"R"
,
List
(
"xt"
,
"st"
)))
assert
(
checkSafeCausal
(
name
,
inv
))
assert
(
checkSafeCausal
NoElim
(
name
,
inv
))
}
it
should
"fail to prove simple causal may things"
in
{
val
name
=
"tests/simpleChoiceCausal"
val
inv
=
Forall
(
List
(
"xt"
),
genEq
(
"S"
,
List
(
"xt"
)))
assert
(!
checkSafeCausal
(
name
,
inv
))
assert
(!
checkSafeCausal
NoElim
(
name
,
inv
))
}
it
should
"fail to prove conference_linear_small"
in
{
...
...
@@ -38,7 +38,7 @@ class InvariantSmallCausalFilesTest extends FlatSpec {
val
yt
=
Var
(
"yt"
,
"X"
)
val
pt
=
Var
(
"pt"
,
"P"
)
val
inv
=
Forall
(
List
(
xt
,
pt
,
yt
),
genEq
(
"Comm"
,
List
(
xt
,
yt
,
pt
)))
assert
(!
checkSafeCausal
(
name
,
inv
))
assert
(!
checkSafeCausal
NoElim
(
name
,
inv
))
}
// it should "fail to prove conference_linear_small with informedness inv" in {
...
...
@@ -54,7 +54,7 @@ class InvariantSmallCausalFilesTest extends FlatSpec {
val
pt
=
Var
(
"pt"
,
"P"
)
val
rt
=
Var
(
"rt"
,
"R"
)
val
inv
=
Forall
(
List
(
xt
,
pt
),
genEq
(
"Conf"
,
List
(
xt
,
pt
)))
assert
(
checkSafeCausal
(
name
,
inv
))
assert
(
checkSafeCausal
NoElim
(
name
,
inv
))
}
it
should
"prove conference_linear_small with trivial inv 2"
in
{
...
...
@@ -64,6 +64,6 @@ class InvariantSmallCausalFilesTest extends FlatSpec {
val
pt
=
Var
(
"pt"
,
"P"
)
val
rt
=
Var
(
"rt"
,
"R"
)
val
inv
=
Forall
(
List
(
xt
,
yt
,
pt
,
rt
),
genEq
(
"Read"
,
List
(
yt
,
pt
,
rt
)))
assert
(!
checkSafeCausal
(
name
,
inv
))
assert
(!
checkSafeCausal
NoElim
(
name
,
inv
))
}
}
\ No newline at end of file
src/test/scala/de/tum/workflows/tests/TestUtils.scala
View file @
0a3d0c62
...
...
@@ -17,19 +17,19 @@ object TestUtils {
}
def
checkSafeStubborn
(
name
:
String
,
desc
:
String
,
inv
:
Formula
)
=
{
check
(
name
,
desc
,
inv
,
InvProperties
(
true
,
true
))
check
(
name
,
desc
,
inv
,
InvProperties
(
true
,
true
,
true
))
}
def
checkSafeCausal
(
name
:
String
,
inv
:
Formula
)
:
Boolean
=
{
checkSafeCausal
(
name
,
""
,
inv
)
def
checkSafeCausal
NoElim
(
name
:
String
,
inv
:
Formula
)
:
Boolean
=
{
checkSafeCausal
NoElim
(
name
,
""
,
inv
)
}
def
checkSafeCausal
(
name
:
String
,
desc
:
String
,
inv
:
Formula
)
=
{
def
checkSafeCausal
NoElim
(
name
:
String
,
desc
:
String
,
inv
:
Formula
)
=
{
check
(
name
,
desc
,
inv
,
InvProperties
(
false
,
false
))
}
def
checkSafeCausalElim
(
name
:
String
,
desc
:
String
,
inv
:
Formula
)
=
{
check
(
name
,
s
"${desc}_elim"
,
inv
,
InvProperties
(
false
,
true
))
check
(
name
,
s
"${desc}_elim"
,
inv
,
InvProperties
(
false
,
true
,
true
))
}
def
genEq
(
name
:
String
,
params
:
List
[
Var
])
=
{
...
...
src/test/scala/de/tum/workflows/tests/papertests/DemoNoStrengtheningTests.scala
View file @
0a3d0c62
...
...
@@ -72,7 +72,7 @@ class DemoNoStrengtheningTests extends FlatSpec {
it
should
"prove tests/simpleChoiceDeclassified causal alleq"
in
{
val
name
=
"tests/simpleChoiceDeclassified"
val
inv
=
InvariantGenerator
.
invariantAllEqual
(
ExampleWorkflows
.
parseExample
(
name
).
get
)
assert
(
checkSafeCausal
(
name
,
"alleq"
,
inv
))
assert
(
checkSafeCausal
NoElim
(
name
,
"alleq"
,
inv
))
}
it
should
"prove tests/simpleChoiceCausal alleq"
in
{
val
name
=
"tests/simpleChoiceCausal"
...
...
@@ -82,6 +82,6 @@ class DemoNoStrengtheningTests extends FlatSpec {
it
should
"prove tests/simpleChoiceCausal causal alleq"
in
{
val
name
=
"tests/simpleChoiceCausal"
val
inv
=
InvariantGenerator
.
invariantNoninterSingleBS
(
ExampleWorkflows
.
parseExample
(
name
).
get
)
assert
(!
checkSafeCausal
(
name
,
"alleq"
,
inv
))
assert
(!
checkSafeCausal
NoElim
(
name
,
"alleq"
,
inv
))
}
}
src/test/scala/de/tum/workflows/tests/papertests/DemoUniversity.scala
View file @
0a3d0c62
...
...
@@ -28,7 +28,7 @@ class DemoUniversityTest extends FlatSpec {
it
should
"prove nonomitting/university causal alleq"
in
{
val
name
=
"nonomitting/university"
val
inv
=
InvariantGenerator
.
invariantNoninterSingleBS
(
ExampleWorkflows
.
parseExample
(
name
).
get
)
assert
(!
checkSafeCausal
(
name
,
"alleq"
,
inv
))
assert
(!
checkSafeCausal
NoElim
(
name
,
"alleq"
,
inv
))
}
}
src/test/scala/de/tum/workflows/tests/papertests/InvariantCausalFilesTest.scala
View file @
0a3d0c62
...
...
@@ -31,7 +31,7 @@ class InvariantCausalFilesTest extends FlatSpec {
it
should
"fail to prove nonomitting/conference_linear alleq"
in
{
val
name
=
"nonomitting/conference_linear"
val
inv
=
InvariantGenerator
.
invariantAllEqual
(
ExampleWorkflows
.
parseExample
(
name
).
get
)
assert
(!
checkSafeCausal
(
name
,
"alleq"
,
inv
))
assert
(!
checkSafeCausal
NoElim
(
name
,
"alleq"
,
inv
))
}
//
// // HEAP SPACE
...
...
@@ -58,7 +58,7 @@ class InvariantCausalFilesTest extends FlatSpec {
it
should
"fail to prove nonomitting/conference alleq"
in
{
val
name
=
"nonomitting/conference"
val
inv
=
InvariantGenerator
.
invariantAllEqual
(
ExampleWorkflows
.
parseExample
(
name
).
get
)
assert
(!
checkSafeCausal
(
name
,
"alleq"
,
inv
))
assert
(!
checkSafeCausal
NoElim
(
name
,
"alleq"
,
inv
))
}
//
// // HEAP SPACE
...
...
@@ -86,7 +86,7 @@ class InvariantCausalFilesTest extends FlatSpec {
it
should
"fail to prove omitting/conference alleq"
in
{
val
name
=
"omitting/conference"
val
inv
=
InvariantGenerator
.
invariantAllEqual
(
ExampleWorkflows
.
parseExample
(
name
).
get
)
assert
(!
checkSafeCausal
(
name
,
"alleq"
,
inv
))
assert
(!
checkSafeCausal
NoElim
(
name
,
"alleq"
,
inv
))
}
// takes forever
...
...
@@ -106,7 +106,7 @@ class InvariantCausalFilesTest extends FlatSpec {
it
should
"prove omitting/conference_linear_fixed alleq"
in
{
val
name
=
"omitting/conference_linear_fixed"
val
inv
=
InvariantGenerator
.
invariantAllEqual
(
ExampleWorkflows
.
parseExample
(
name
).
get
)
assert
(
checkSafeCausal
(
name
,
"alleq"
,
inv
))
assert
(
checkSafeCausal
NoElim
(
name
,
"alleq"
,
inv
))
}
it
should
"prove omitting/conference_linear_fixed_stubborn alleq noelim"
in
{
...
...
@@ -124,7 +124,7 @@ class InvariantCausalFilesTest extends FlatSpec {
it
should
"prove omitting/conference_fixed alleq"
in
{
val
name
=
"omitting/conference_fixed"
val
inv
=
InvariantGenerator
.
invariantAllEqual
(
ExampleWorkflows
.
parseExample
(
name
).
get
)
assert
(
checkSafeCausal
(
name
,
"alleq"
,
inv
))
assert
(
checkSafeCausal
NoElim
(
name
,
"alleq"
,
inv
))
}
...
...
Write
Preview
Markdown
is supported
0%
Try again
or
attach a new file
Attach a file
Cancel
You are about to add
0
people
to the discussion. Proceed with caution.
Finish editing this message first!
Cancel
Please
register
or
sign in
to comment