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
4466e442
Commit
4466e442
authored
Jul 06, 2017
by
Eugen Zalinescu
Browse files
Options
Browse Files
Download
Email Patches
Plain Diff
works for Globally; Term -> Formula
parent
e59e0ae8
Changes
10
Hide whitespace changes
Inline
Side-by-side
Showing
10 changed files
with
274 additions
and
145 deletions
+274
-145
src/main/scala/de/tum/workflows/Encoding.scala
src/main/scala/de/tum/workflows/Encoding.scala
+2
-2
src/main/scala/de/tum/workflows/Main.scala
src/main/scala/de/tum/workflows/Main.scala
+3
-3
src/main/scala/de/tum/workflows/WorkflowParser.scala
src/main/scala/de/tum/workflows/WorkflowParser.scala
+1
-1
src/main/scala/de/tum/workflows/blocks/Workflow.scala
src/main/scala/de/tum/workflows/blocks/Workflow.scala
+4
-4
src/main/scala/de/tum/workflows/foltl/FOLTL.scala
src/main/scala/de/tum/workflows/foltl/FOLTL.scala
+43
-43
src/main/scala/de/tum/workflows/foltl/FOLTLTermFunctions.scala
...ain/scala/de/tum/workflows/foltl/FOLTLTermFunctions.scala
+13
-13
src/main/scala/de/tum/workflows/foltl/Properties.scala
src/main/scala/de/tum/workflows/foltl/Properties.scala
+2
-2
src/main/scala/de/tum/workflows/ltl/LTL.scala
src/main/scala/de/tum/workflows/ltl/LTL.scala
+6
-6
src/main/scala/de/tum/workflows/toz3/toz3.scala
src/main/scala/de/tum/workflows/toz3/toz3.scala
+168
-56
src/test/scala/de/tum/workflows/ltl/tests/Z3Test.scala
src/test/scala/de/tum/workflows/ltl/tests/Z3Test.scala
+32
-15
No files found.
src/main/scala/de/tum/workflows/Encoding.scala
View file @
4466e442
...
...
@@ -9,7 +9,7 @@ import scalax.collection.edge.Implicits._ // shortcuts
import
blocks._
import
de.tum.workflows.foltl.FOLTL
import
de.tum.workflows.foltl.FOLTL._
import
de.tum.workflows.foltl.
Term
Functions._
import
de.tum.workflows.foltl.
Formula
Functions._
import
com.typesafe.scalalogging._
...
...
@@ -113,7 +113,7 @@ object Encoding extends LazyLogging {
And
.
make
(
nodeVar
(
0
),
And
.
make
(
nodes
),
Globally
(
And
.
make
(
negs
)))
}
def
encodeStmt
(
s
:
Statement
,
pred
:
Option
[
Term
],
bind
:
List
[
Var
])
:
(
Term
,
String
)
=
{
def
encodeStmt
(
s
:
Statement
,
pred
:
Option
[
Formula
],
bind
:
List
[
Var
])
:
(
Formula
,
String
)
=
{
// var guard = s.guard
// for (p <- pred) { // if pred defined
// guard = And(guard, p)
...
...
src/main/scala/de/tum/workflows/Main.scala
View file @
4466e442
...
...
@@ -12,7 +12,7 @@ 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.
Term
Functions
import
de.tum.workflows.foltl.
Formula
Functions
object
Main
extends
App
with
LazyLogging
{
...
...
@@ -40,14 +40,14 @@ object Main extends App with LazyLogging {
writer
.
close
()
}
def
writeExample
(
name
:
String
,
spec
:
Spec
,
prop
:
Term
)
{
def
writeExample
(
name
:
String
,
spec
:
Spec
,
prop
:
Formula
)
{
var
metrics
=
List
[
String
]()
write
(
s
"${name}.foltl"
,
prop
.
pretty
())
metrics
:+=
s
"${name}.foltl: ${prop.opsize()}"
if
(!
Term
Functions
.
checkSanity
(
prop
))
{
if
(!
Formula
Functions
.
checkSanity
(
prop
))
{
logger
.
error
(
"Property didn't pass sanity check"
)
return
}
...
...
src/main/scala/de/tum/workflows/WorkflowParser.scala
View file @
4466e442
...
...
@@ -135,7 +135,7 @@ object WorkflowParser extends RegexParsers with LazyLogging {
def
FUN
=
VAR
~
TUPLE
^^
{
case
f
~
tup
=>
Fun
(
f
.
name
,
tup
)
}
def
SIMPLETERM
=
(
tt
|
ff
|
FUN
)
def
TERM
:
Parser
[
Term
]
=
(
SIMPLETERM
|
GLOBALLY
|
FINALLY
|
AND
|
OR
|
NEG
)
def
TERM
:
Parser
[
Formula
]
=
(
SIMPLETERM
|
GLOBALLY
|
FINALLY
|
AND
|
OR
|
NEG
)
def
ADD
=
TERM
~
(
"→"
|
"->"
)
~
VAR
~
"+="
~
TUPLE
^^
{
case
guard
~
_
~
fun
~
_
~
tup
=>
Add
(
guard
,
fun
.
name
,
tup
)
}
def
REM
=
TERM
~
(
"→"
|
"->"
)
~
VAR
~
"-="
~
TUPLE
^^
{
case
guard
~
_
~
fun
~
_
~
tup
=>
Remove
(
guard
,
fun
.
name
,
tup
)
}
...
...
src/main/scala/de/tum/workflows/blocks/Workflow.scala
View file @
4466e442
...
...
@@ -19,7 +19,7 @@ object Workflow {
val
EMPTY
=
Workflow
(
Signature
.
EMPTY
,
List
())
}
case
class
Spec
(
w
:
Workflow
,
declass
:
List
[(
Fun
,
Term
)],
target
:
Fun
,
causals
:
List
[
Var
])
extends
LazyLogging
{
case
class
Spec
(
w
:
Workflow
,
declass
:
List
[(
Fun
,
Formula
)],
target
:
Fun
,
causals
:
List
[
Var
])
extends
LazyLogging
{
override
def
toString
=
{
s
"Spec\nWorkflow:\n$w\nDeclass:$declass\nTarget:$target"
}
...
...
@@ -62,17 +62,17 @@ abstract sealed class SimpleBlock extends Block {
}
abstract
class
Statement
{
def
guard
:
Term
def
guard
:
Formula
def
fun
:
String
def
tuple
:
List
[
Var
]
def
freeVars
()
=
guard
.
freeVars
()
++
tuple
}
case
class
Add
(
guard
:
Term
,
fun
:
String
,
tuple
:
List
[
Var
])
extends
Statement
{
case
class
Add
(
guard
:
Formula
,
fun
:
String
,
tuple
:
List
[
Var
])
extends
Statement
{
override
def
toString
()
=
guard
+
" → "
+
fun
+
" += "
+
tuple
.
mkString
(
"("
,
","
,
")"
)
+
";"
}
case
class
Remove
(
guard
:
Term
,
fun
:
String
,
tuple
:
List
[
Var
])
extends
Statement
{
case
class
Remove
(
guard
:
Formula
,
fun
:
String
,
tuple
:
List
[
Var
])
extends
Statement
{
override
def
toString
()
=
guard
+
" → "
+
fun
+
" -= "
+
tuple
.
mkString
(
"("
,
","
,
")"
)
+
";"
}
...
...
src/main/scala/de/tum/workflows/foltl/FOLTL.scala
View file @
4466e442
...
...
@@ -6,15 +6,15 @@ import scala.annotation.tailrec
//import de.tum.workflows.foltl.TermFunctions._
object
FOLTL
{
abstract
class
Term
{
def
simplify
()
=
Term
Functions
.
simplify
(
this
)
def
freeVars
()
=
Term
Functions
.
freeVars
(
this
)
def
everywhere
(
trans
:
PartialFunction
[
Term
,
Term
])
=
Term
Functions
.
everywhere
(
trans
,
this
)
def
assumeEmpty
(
name
:
String
)
=
Term
Functions
.
assumeEmpty
(
this
,
name
)
def
in
(
name
:
String
)
=
Term
Functions
.
annotate
(
this
,
name
)
def
in
(
name
:
String
,
ignore
:
Set
[
String
])
=
Term
Functions
.
annotate
(
this
,
name
,
ignore
)
def
collect
[
T
](
coll
:
PartialFunction
[
Term
,
List
[
T
]])
=
Term
Functions
.
collect
(
coll
,
this
)
def
opsize
()
=
Term
Functions
.
opsize
(
this
)
abstract
class
Formula
{
def
simplify
()
=
Formula
Functions
.
simplify
(
this
)
def
freeVars
()
=
Formula
Functions
.
freeVars
(
this
)
def
everywhere
(
trans
:
PartialFunction
[
Formula
,
Formula
])
=
Formula
Functions
.
everywhere
(
trans
,
this
)
def
assumeEmpty
(
name
:
String
)
=
Formula
Functions
.
assumeEmpty
(
this
,
name
)
def
in
(
name
:
String
)
=
Formula
Functions
.
annotate
(
this
,
name
)
def
in
(
name
:
String
,
ignore
:
Set
[
String
])
=
Formula
Functions
.
annotate
(
this
,
name
,
ignore
)
def
collect
[
T
](
coll
:
PartialFunction
[
Formula
,
List
[
T
]])
=
Formula
Functions
.
collect
(
coll
,
this
)
def
opsize
()
=
Formula
Functions
.
opsize
(
this
)
def
bracketed
()
:
String
=
this
match
{
case
_:
BinOp
=>
"("
+
this
+
")"
...
...
@@ -40,13 +40,13 @@ object FOLTL {
}
}
case
object
True
extends
Term
case
object
False
extends
Term
case
object
True
extends
Formula
case
object
False
extends
Formula
object
Var
{
val
DEFAULT_TYPE
=
"T"
}
case
class
Var
(
name
:
String
,
typ
:
String
=
Var
.
DEFAULT_TYPE
)
extends
Term
{
case
class
Var
(
name
:
String
,
typ
:
String
=
Var
.
DEFAULT_TYPE
)
extends
Formula
{
override
def
toString
()
=
s
"$name"
def
withType
()
=
s
"$name:$typ"
}
...
...
@@ -54,17 +54,17 @@ object FOLTL {
object
Fun
{
def
apply
(
name
:
String
,
params
:
List
[
Var
])
:
Fun
=
Fun
(
name
,
None
,
params
)
}
case
class
Fun
(
name
:
String
,
ind
:
Option
[
String
],
params
:
List
[
Var
])
extends
Term
{
case
class
Fun
(
name
:
String
,
ind
:
Option
[
String
],
params
:
List
[
Var
])
extends
Formula
{
override
def
toString
()
=
name
+
Utils
.
mkString
(
ind
,
"("
,
""
,
")"
)
+
params
.
map
(
_
.
name
).
mkString
(
"("
,
","
,
")"
)
def
updatedParams
(
index
:
Int
,
p
:
Var
)
=
Fun
(
name
,
ind
,
params
.
updated
(
index
,
p
))
def
updatedParams
(
list
:
List
[
Var
])
=
Fun
(
name
,
ind
,
list
)
}
trait
Quantifier
extends
Term
{
def
qmake
:
(
List
[
Var
],
Term
)
=>
Quantifier
trait
Quantifier
extends
Formula
{
def
qmake
:
(
List
[
Var
],
Formula
)
=>
Quantifier
def
qname
:
String
def
vars
:
List
[
Var
]
def
t
:
Term
def
t
:
Formula
override
def
toString
()
=
{
// show types only in quantifiers
...
...
@@ -76,51 +76,51 @@ object FOLTL {
def
unapply
(
q
:
Quantifier
)
=
Some
((
q
.
qmake
,
q
.
vars
,
q
.
t
))
}
case
class
Exists
(
vars
:
List
[
Var
],
t
:
Term
)
extends
Quantifier
{
case
class
Exists
(
vars
:
List
[
Var
],
t
:
Formula
)
extends
Quantifier
{
val
qname
=
"∃"
val
qmake
=
Exists
.
apply
_
}
case
class
Forall
(
vars
:
List
[
Var
],
t
:
Term
)
extends
Quantifier
{
case
class
Forall
(
vars
:
List
[
Var
],
t
:
Formula
)
extends
Quantifier
{
val
qname
=
"∀"
val
qmake
=
Forall
.
apply
_
}
case
class
ForallOtherThan
(
vars
:
List
[
Var
],
otherthan
:
List
[
Var
],
t
:
Term
)
extends
Quantifier
{
case
class
ForallOtherThan
(
vars
:
List
[
Var
],
otherthan
:
List
[
Var
],
t
:
Formula
)
extends
Quantifier
{
val
qname
=
"∀"
val
qmake
=
ForallOtherThan
.
apply
(
_:
List
[
Var
],
otherthan
,
_:
Term
)
val
qmake
=
ForallOtherThan
.
apply
(
_:
List
[
Var
],
otherthan
,
_:
Formula
)
override
def
toString
()
=
{
s
"$qname ${vars.map(_.withType()).mkString("
,
")} ∉ {${otherthan.map(_.withType()).mkString("
,
")}}. ${t.bracketed()}"
}
}
trait
Temporal
Term
extends
Term
trait
Temporal
Formula
extends
Formula
case
class
Next
(
t
:
Term
)
extends
TemporalTerm
with
UnOp
{
case
class
Next
(
t
:
Formula
)
extends
TemporalFormula
with
UnOp
{
val
make
=
Next
.
apply
_
val
opname
=
"X"
}
case
class
Globally
(
t
:
Term
)
extends
TemporalTerm
with
UnOp
{
case
class
Globally
(
t
:
Formula
)
extends
TemporalFormula
with
UnOp
{
val
make
=
Globally
.
apply
_
val
opname
=
"G"
}
case
class
Finally
(
t
:
Term
)
extends
TemporalTerm
with
UnOp
{
case
class
Finally
(
t
:
Formula
)
extends
TemporalFormula
with
UnOp
{
val
make
=
Finally
.
apply
_
val
opname
=
"F"
}
case
class
Until
(
t1
:
Term
,
t2
:
Term
)
extends
TemporalTerm
with
BinOp
{
case
class
Until
(
t1
:
Formula
,
t2
:
Formula
)
extends
TemporalFormula
with
BinOp
{
val
make
=
Until
.
apply
_
val
opname
=
"U"
}
object
WUntil
{
def
apply
(
t1
:
Term
,
t2
:
Term
)
=
Or
(
Until
(
t1
,
t2
),
Globally
(
t1
))
def
apply
(
t1
:
Formula
,
t2
:
Formula
)
=
Or
(
Until
(
t1
,
t2
),
Globally
(
t1
))
}
trait
UnOp
extends
Term
{
def
make
:
Term
=>
UnOp
trait
UnOp
extends
Formula
{
def
make
:
Formula
=>
UnOp
def
opname
:
String
def
t
:
Term
def
t
:
Formula
override
def
toString
()
=
opname
+
" "
+
t
.
bracketed
()
}
...
...
@@ -131,11 +131,11 @@ object FOLTL {
}
}
trait
BinOp
extends
Term
{
def
make
:
(
Term
,
Term
)
=>
BinOp
trait
BinOp
extends
Formula
{
def
make
:
(
Formula
,
Formula
)
=>
BinOp
def
opname
:
String
def
t1
:
Term
def
t2
:
Term
def
t1
:
Formula
def
t2
:
Formula
override
def
toString
()
=
{
(
t1
,
t2
)
match
{
...
...
@@ -152,7 +152,7 @@ object FOLTL {
Some
((
binop
.
make
,
binop
.
t1
,
binop
.
t2
))
}
def
makeL
(
make
:
(
Term
,
Term
)
=>
Term
,
l
:
Seq
[
Term
],
Empty
:
Term
)
:
Term
=
{
def
makeL
(
make
:
(
Formula
,
Formula
)
=>
Formula
,
l
:
Seq
[
Formula
],
Empty
:
Formula
)
:
Formula
=
{
l
.
toList
match
{
case
List
(
x
)
=>
x
case
Empty
::
xs
=>
makeL
(
make
,
xs
,
Empty
)
...
...
@@ -163,44 +163,44 @@ object FOLTL {
}
object
Or
{
def
make
(
terms
:
List
[
Term
])
=
{
def
make
(
terms
:
List
[
Formula
])
=
{
BinOp
.
makeL
(
Or
.
apply
_
,
terms
,
True
)
}
def
make
(
terms
:
Term
*
)
=
{
def
make
(
terms
:
Formula
*
)
=
{
BinOp
.
makeL
(
Or
.
apply
_
,
terms
,
False
)
}
}
case
class
Or
(
t1
:
Term
,
t2
:
Term
)
extends
BinOp
{
case
class
Or
(
t1
:
Formula
,
t2
:
Formula
)
extends
BinOp
{
val
opname
=
"∨"
val
make
=
Or
.
apply
_
}
object
And
{
def
make
(
terms
:
List
[
Term
])
=
{
def
make
(
terms
:
List
[
Formula
])
=
{
BinOp
.
makeL
(
And
.
apply
_
,
terms
,
True
)
}
def
make
(
terms
:
Term
*
)
=
{
def
make
(
terms
:
Formula
*
)
=
{
BinOp
.
makeL
(
And
.
apply
_
,
terms
,
True
)
}
}
case
class
And
(
t1
:
Term
,
t2
:
Term
)
extends
BinOp
{
case
class
And
(
t1
:
Formula
,
t2
:
Formula
)
extends
BinOp
{
val
opname
=
"∧"
val
make
=
And
.
apply
_
}
case
class
Eq
(
t1
:
Term
,
t2
:
Term
)
extends
BinOp
{
case
class
Eq
(
t1
:
Formula
,
t2
:
Formula
)
extends
BinOp
{
val
opname
=
"↔"
val
make
=
Eq
.
apply
_
}
case
class
Implies
(
t1
:
Term
,
t2
:
Term
)
extends
BinOp
{
case
class
Implies
(
t1
:
Formula
,
t2
:
Formula
)
extends
BinOp
{
val
opname
=
"→"
val
make
=
Implies
.
apply
_
}
case
class
Neg
(
t
:
Term
)
extends
UnOp
{
case
class
Neg
(
t
:
Formula
)
extends
UnOp
{
val
make
=
Neg
.
apply
_
val
opname
=
"¬"
}
...
...
src/main/scala/de/tum/workflows/foltl/FOLTLTermFunctions.scala
View file @
4466e442
...
...
@@ -3,10 +3,10 @@ package de.tum.workflows.foltl
import
FOLTL._
import
com.typesafe.scalalogging.LazyLogging
object
Term
Functions
extends
LazyLogging
{
object
Formula
Functions
extends
LazyLogging
{
def
freeVars
(
t
:
Term
)
=
{
def
free
(
t
:
Term
,
bound
:
Set
[
Var
])
:
Set
[
Var
]
=
{
def
freeVars
(
t
:
Formula
)
=
{
def
free
(
t
:
Formula
,
bound
:
Set
[
Var
])
:
Set
[
Var
]
=
{
t
match
{
// Extractors
// Exists, Forall
...
...
@@ -24,8 +24,8 @@ object TermFunctions extends LazyLogging {
free
(
t
,
Set
())
}
def
simplify
(
t
:
Term
)
:
Term
=
{
val
simp
:
PartialFunction
[
Term
,
Term
]
=
{
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
))
...
...
@@ -76,7 +76,7 @@ object TermFunctions extends LazyLogging {
if
(
t
==
t1
)
t1
else
simplify
(
t1
)
}
def
everywhere
(
trans
:
PartialFunction
[
Term
,
Term
],
t
:
Term
)
:
Term
=
{
def
everywhere
(
trans
:
PartialFunction
[
Formula
,
Formula
],
t
:
Formula
)
:
Formula
=
{
if
(
trans
.
isDefinedAt
(
t
))
trans
(
t
)
else
...
...
@@ -89,7 +89,7 @@ object TermFunctions extends LazyLogging {
}
}
def
opsize
(
t
:
Term
)
:
Int
=
{
def
opsize
(
t
:
Formula
)
:
Int
=
{
t
match
{
// Extractors
case
Quantifier
(
_
,
ps
,
t
)
=>
1
+
t
.
opsize
()
...
...
@@ -99,7 +99,7 @@ object TermFunctions extends LazyLogging {
}
}
def
collect
[
T
](
combine
:
(
T*
)
=>
T
,
empty
:
T
)(
coll
:
PartialFunction
[
Term
,
T
],
t
:
Term
)
:
T
=
{
def
collect
[
T
](
combine
:
(
T*
)
=>
T
,
empty
:
T
)(
coll
:
PartialFunction
[
Formula
,
T
],
t
:
Formula
)
:
T
=
{
if
(
coll
.
isDefinedAt
(
t
))
coll
(
t
)
else
...
...
@@ -112,7 +112,7 @@ object TermFunctions extends LazyLogging {
}
}
def
collect
[
T
](
coll
:
PartialFunction
[
Term
,
List
[
T
]],
t
:
Term
)
:
List
[
T
]
=
{
def
collect
[
T
](
coll
:
PartialFunction
[
Formula
,
List
[
T
]],
t
:
Formula
)
:
List
[
T
]
=
{
if
(
coll
.
isDefinedAt
(
t
))
coll
(
t
)
else
...
...
@@ -125,25 +125,25 @@ object TermFunctions extends LazyLogging {
}
}
def
assumeEmpty
(
t
:
Term
,
name
:
String
)
=
{
def
assumeEmpty
(
t
:
Formula
,
name
:
String
)
=
{
t
.
everywhere
({
case
Fun
(
f
,
_
,
_
)
if
f
==
name
=>
False
})
}
def
annotate
(
t
:
Term
,
name
:
String
)
=
{
def
annotate
(
t
:
Formula
,
name
:
String
)
=
{
t
.
everywhere
({
case
Fun
(
f
,
None
,
xs
)
=>
Fun
(
f
,
Some
(
name
),
xs
)
})
}
def
annotate
(
t
:
Term
,
name
:
String
,
ignore
:
Set
[
String
])
=
{
def
annotate
(
t
:
Formula
,
name
:
String
,
ignore
:
Set
[
String
])
=
{
t
.
everywhere
({
case
Fun
(
f
,
None
,
xs
)
if
(!(
ignore
contains
f
))
=>
Fun
(
f
,
Some
(
name
),
xs
)
})
}
def
checkSanity
(
t
:
Term
)
=
{
def
checkSanity
(
t
:
Formula
)
=
{
// TODO add more things, f.e. existentials
// T1, T2 can appear freely
val
frees
=
t
.
freeVars
()
--
Set
(
Var
(
Properties
.
T1
),
Var
(
Properties
.
T2
))
...
...
src/main/scala/de/tum/workflows/foltl/Properties.scala
View file @
4466e442
...
...
@@ -67,10 +67,10 @@ object Causal {
object
Noninterference
extends
LazyLogging
{
def
buildViolations
(
vars
:
List
[
Var
],
t
:
Term
,
causals
:
List
[
Var
])
=
{
def
buildViolations
(
vars
:
List
[
Var
],
t
:
Formula
,
causals
:
List
[
Var
])
=
{
val
univ
=
causals
.
groupBy
(
_
.
typ
).
withDefault
(
_
=>
List
())
def
build
(
agents
:
List
[
Var
],
t
:
Term
)
:
List
[
Term
]
=
{
def
build
(
agents
:
List
[
Var
],
t
:
Formula
)
:
List
[
Formula
]
=
{
agents
match
{
case
x
::
xs
=>
{
...
...
src/main/scala/de/tum/workflows/ltl/LTL.scala
View file @
4466e442
...
...
@@ -25,9 +25,9 @@ object LTL extends LazyLogging {
}
}
def
eliminateExistentials
(
t
:
Term
)
=
{
def
eliminateExistentials
(
t
:
Formula
)
=
{
def
coll
:
PartialFunction
[
Term
,
List
[
Var
]]
=
{
def
coll
:
PartialFunction
[
Formula
,
List
[
Var
]]
=
{
case
Exists
(
a
,
term
)
=>
a
++
term
.
collect
(
coll
)
// don't go over Foralls
case
Forall
(
_
,
_
)
=>
List
.
empty
...
...
@@ -37,7 +37,7 @@ object LTL extends LazyLogging {
}
val
agents
=
t
.
collect
(
coll
)
def
elim
:
PartialFunction
[
Term
,
Term
]
=
{
def
elim
:
PartialFunction
[
Formula
,
Formula
]
=
{
case
Exists
(
a
,
term
)
=>
term
.
everywhere
(
elim
)
// don't go over Foralls
case
term
:
Forall
=>
term
...
...
@@ -51,14 +51,14 @@ object LTL extends LazyLogging {
(
agents
,
res
)
}
def
eliminateUniversals
(
t
:
Term
,
agents
:
List
[
Var
])
:
Term
=
{
def
eliminateUniversals
(
t
:
Formula
,
agents
:
List
[
Var
])
:
Formula
=
{
if
(
agents
.
isEmpty
)
{
logger
.
error
(
"Agent list should never be empty"
)
}
val
universe
=
agents
.
groupBy
(
_
.
typ
)
def
instantiate
(
tup
:
List
[
Var
],
t
:
Term
,
universe
:
Map
[
String
,
List
[
FOLTL.Var
]])
=
{
def
instantiate
(
tup
:
List
[
Var
],
t
:
Formula
,
universe
:
Map
[
String
,
List
[
FOLTL.Var
]])
=
{
if
(!
tup
.
forall
(
v
=>
universe
.
contains
(
v
.
typ
)))
{
// everything is valid for quantifiers over empty sets
logger
.
warn
(
s
"Ignored ${Forall(tup, t)} (empty universe for at least one type)"
)
...
...
@@ -90,7 +90,7 @@ object LTL extends LazyLogging {
})
}
def
eliminatePredicates
(
t
:
Term
)
=
{
def
eliminatePredicates
(
t
:
Formula
)
=
{
t
.
everywhere
({
case
Fun
(
f
,
ind
,
tup
)
=>
{
val
pi
=
if
(
ind
.
isDefined
)
"_"
+
ind
.
get
else
""
...
...
src/main/scala/de/tum/workflows/toz3/toz3.scala
View file @
4466e442
...
...
@@ -2,74 +2,186 @@ package de.tum.workflows.toz3;
import
de.tum.workflows.foltl.FOLTL
import
de.tum.workflows.foltl.FOLTL._
import
de.tum.workflows.foltl.
Term
Functions._
import
de.tum.workflows.foltl.
Formula
Functions._
import
com.microsoft.z3._
;
// import collection.mutable.HashMap
import
java.util.concurrent.atomic.AtomicInteger
import
java.util.HashMap
import
com.typesafe.scalalogging.LazyLogging
object
Test
extends
App
{
def
toZ3
(
ctx
:
Context
,
t
:
Term
)
=
{
t
match
{
case
t
:
Var
=>
{
ctx
.
mkSymbol
(
t
.
name
)
object
toZ3
extends
LazyLogging
{
def
succ
(
ctx
:
Context
,
e
:
ArithExpr
)
=
{
val
One
=
ctx
.
mkInt
(
1
)
ctx
.
mkAdd
(
e
,
One
)
}
var
counter
=
0
val
fun_ctx
=
new
HashMap
[
String
,
FuncDecl
]()
def
new_tvar
(
ctx
:
Context
)
=
{
counter
=
counter
+
1
"t"
+
counter
}
// def getSort(ctx: Context, typ: String) = {
// if (!sort_ctx.isDefinedAt(typ)) {
// // TODO: size of the finite domain?!
// val s = ctx.mkFiniteDomainSort(typ, 2)
// sort_ctx += (typ -> s)
// }
// sort_ctx(typ)
// }
def
buildVarCtx
(
ctx
:
Context
,
var_ctx
:
Map
[
Var
,
(
Int
,
Expr
,
Sort
)],
vars
:
List
[
Var
])
=
{
val
newexprs
=
(
for
((
v
,
i
)
<-
vars
.
zip
(
vars
.
size
-
1
to
0
))
yield
{
// TODO: size?
val
sort
=
if
(
v
.
typ
.
equals
(
"Int"
))
{
ctx
.
getIntSort
()
}
else
if
(
v
.
typ
.
equals
(
"Bool"
))
{
ctx
.
getBoolSort
()
}
else
{
ctx
.
mkFiniteDomainSort
(
v
.
typ
,
2
)
}
}
v
->
(
i
,
ctx
.
mkBound
(
i
,
sort
),
sort
)
})
toMap
val
oldvars
=
(
for
((
v
,
(
i
,
e
,
s
))
<-
var_ctx
)
yield
{
val
newi
=
i
+
vars
.
size
val
newbound
=
ctx
.
mkBound
(
newi
,
s
)
v
->
(
newi
,
newbound
,
s
)
})
newexprs
++
oldvars
}
class
TestFailedException
extends
Exception
{}
def
check
(
ctx
:
Context
,
f
:
BoolExpr
,
sat
:
Status
)
:
(
Model
)
=
{
val
s
=
ctx
.
mkSolver
()
s
.
add
(
f
)
if
(
s
.
check
()
!=
sat
)
throw
new
TestFailedException
();
if
(
sat
==
Status
.
SATISFIABLE
)
return
s
.
getModel
();
else
return
null
;
def
updateTime
(
tvar
:
Option
[
Var
],
texpr
:
ArithExpr
,
oldctx
:
Map
[
Var
,
(
Int
,
Expr
,
Sort
)],
newctx
:
Map
[
Var
,
(
Int
,
Expr
,
Sort
)])
=
{
if
(
tvar
.
isEmpty
)
{
texpr
}
else
{
texpr
.
substitute
(
oldctx
(
tvar
.
get
).
_2
,
newctx
(
tvar
.
get
).
_2
).
asInstanceOf
[
ArithExpr
]
}
}
def
atest
(
ctx
:
Context
)
=
{
val
x
=
ctx
.
mkIntConst
(
"x"
)
val
y
=
ctx
.
mkIntConst
(
"y"
)
val
one
=
ctx
.
mkInt
(
1
)
val
two
=
ctx
.
mkInt
(
2
)
val
y_plus_one
=
ctx
.
mkAdd
(
y
,
one
)
def
toZ3
(
ctx
:
Context
,
f
:
Formula
,
texpr
:
ArithExpr
,
tvar
:
Option
[
Var
],
var_ctx
:
Map
[
Var
,
(
Int
,
Expr
,
Sort
)])
:
BoolExpr
=
{
// tvar can be an expression e with the form
// given by the following grammar:
// e ::= 0 | t | succ(e)
f
match
{
// case v: Var => // TODO
case
Fun
(
name
,
ind
,
params
)
=>
{
var
fdecl
=
fun_ctx
.
get
(
name
)
if
(
fdecl
==
null
)
{
val
pi
=
if
(
ind
.
isDefined
)
"_"
+
ind
.
get
else
""
val
sorts
=
params
.
map
(
x
=>
var_ctx
(
x
).
_3
)
// first sort is Int, as it stores time values
val
new_sorts
=
(
ctx
.
getIntSort
()
::
sorts
).
toArray
[
Sort
]
fdecl
=
ctx
.
mkFuncDecl
(
name
+
pi
,
new_sorts
,
ctx
.
getBoolSort
())
fun_ctx
.
put
(
name
,
fdecl
)
}
// all variables should be quantified, so they should be part of var_ctx
val
all_args
=
texpr
::
params
.
map
(
x
=>
var_ctx
(
x
).
_2
)
fdecl
.
apply
(
all_args
:
_
*
).
asInstanceOf
[
BoolExpr
]
}
case
Next
(
f1
)
=>
{
toZ3
(
ctx
,
f1
,
succ
(
ctx
,
texpr
),
tvar
,
var_ctx
)
}
case
Globally
(
f1
)
=>
{
val
newt
=
new_tvar
(
ctx
)
val
quantifiername
=
"G"
+
counter
val
sortInt
=
ctx
.
getIntSort
()
val
c1
=
ctx
.
mkLt
(
x
,
y_plus_one
)
val
c2
=
ctx
.
mkGt
(
x
,
two
)
val
variable
=
Var
(
newt
,
"Int"
)
val
q
=
ctx
.
mkAnd
(
c1
,
c2
)
val
newctx
=
buildVarCtx
(
ctx
,
var_ctx
,
List
(
variable
)
)
System
.
out
.
println
(
"model for: x < y + 1, x > 2"
)
val
model
=
check
(
ctx
,
q
,
Status
.
SATISFIABLE
)
System
.
out
.
println
(
"x = "
+
model
.
evaluate
(
x
,
false
)
+
", y = "
+
model
.
evaluate
(
y
,
false
))
val
new_texpr
=
newctx
(
variable
).
_2
.
asInstanceOf
[
ArithExpr
]
val
e1
=
toZ3
(
ctx
,
f1
,
new_texpr
,
Some
(
variable
),
newctx
)
// replace old timevar in old ctx by new timevar
val
old_texpr
=
updateTime
(
tvar
,
texpr
,
var_ctx
,
newctx
)
val
e0
=
ctx
.
mkLe
(
old_texpr
,
new_texpr
.
asInstanceOf
[
ArithExpr
])
val
body
=
ctx
.
mkImplies
(
e0
,
e1
)
ctx
.
mkForall
(
Array
(
sortInt
),
Array
(
ctx
.
mkSymbol
(
newt
)),
body
,
0
,
null
,
null
,
ctx
.
mkSymbol
(
quantifiername
),
null
)
}
// case Finally(f1) => {
//
// }
//
// case Until(f1, f2) => {
//
// }
case
FOLTL
.
Exists
(
vars
,
f1
)
=>
{
val
names
:
Array
[
Symbol
]
=
vars
.
map
(
v
=>
ctx
.
mkSymbol
(
v
.
name
))
toArray
val
newctx
=
buildVarCtx
(
ctx
,
var_ctx
,
vars
)
val
sorts
=
vars
.
map
(
newctx
(
_
).
_3
)
toArray
val
upd_texpr
=
updateTime
(
tvar
,
texpr
,
var_ctx
,
newctx
)
val
e1
=
toZ3
(
ctx
,
f1
,
upd_texpr
,
tvar
,
newctx
)
ctx
.
mkExists
(
sorts
,
names
,
e1
,
0
,
null
,
null
,
null
,
null
)
}
case
FOLTL
.
Forall
(
vars
,
f1
)
=>
{
val
names
:
Array
[
Symbol
]
=
vars
.
map
(
v
=>
ctx
.
mkSymbol
(
v
.
name
))
toArray
val
newctx
=
buildVarCtx
(
ctx
,
var_ctx
,
vars
)
val
sorts
=
vars
.
map
(
newctx
(
_
).
_3
)
toArray
val
upd_texpr
=
updateTime
(
tvar
,
texpr
,
var_ctx
,
newctx
)
val
e1
=
toZ3
(
ctx
,
f1
,
upd_texpr
,
tvar
,
newctx
)
ctx
.
mkForall
(
sorts
,
names
,
e1
,
0
,
null
,
null
,
null
,
null
)
}
// TODO: forallotherthan
case
And
(
f1
,
f2
)
=>
{
val
e1
=
toZ3
(
ctx
,
f1
,
texpr
,
tvar
,
var_ctx
)
val
e2
=
toZ3
(
ctx
,
f2
,
texpr
,
tvar
,
var_ctx
)
ctx
.
mkAnd
(
e1
,
e2
)
}
case
Or
(
f1
,
f2
)
=>
{
val
e1
=
toZ3
(
ctx
,
f1
,
texpr
,
tvar
,
var_ctx
)
val
e2
=
toZ3
(
ctx
,
f2
,
texpr
,
tvar
,
var_ctx
)
ctx
.
mkOr
(
e1
,
e2
)
}
case
Implies
(
f1
,
f2
)
=>
{
val
e1
=
toZ3
(
ctx
,
f1
,
texpr
,
tvar
,
var_ctx
)
val
e2
=
toZ3
(
ctx
,
f2
,
texpr
,
tvar
,
var_ctx
)
ctx
.
mkImplies
(
e1
,
e2
)
}
case
Neg
(
f1
)
=>
{
val
e
=
toZ3
(
ctx
,
f1
,
texpr
,
tvar
,
var_ctx
)
ctx
.
mkNot
(
e
)
}
}
}
def
main
()
=
{
com
.
microsoft
.
z3
.
Global
.
ToggleWarningMessages
(
true
);
// Log.open("test.log");
System
.
out
.
print
(
"Z3 Major Version: "
);
System
.
out
.
println
(
Version
.
getMajor
());
System
.
out
.
print
(
"Z3 Full Version: "
);
System
.
out
.
println
(
Version
.
getString
());
System
.
out
.
print
(
"Z3 Full Version String: "
);
System
.
out
.
println
(
Version
.
getFullVersion
());
val
cfg
=
new
HashMap
[
String
,
String
]();
cfg
.
put
(
"model"
,
"true"
);
val
ctx
=
new
Context
(
cfg
);
atest
(
ctx
);
def
checkZ3
(
f
:
Formula
)
=
{
val
cfg
=
new
HashMap
[
String
,
String
]();
cfg
.
put
(
"model"
,
"true"
);
val
ctx
=
new
Context
(
cfg
);