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
14b736c7
Commit
14b736c7
authored
Mar 07, 2019
by
Christian Müller
Browse files
Options
Browse Files
Download
Email Patches
Plain Diff
leaders
parent
2c08691d
Changes
14
Hide whitespace changes
Inline
Side-by-side
Showing
14 changed files
with
271 additions
and
143 deletions
+271
-143
src/main/scala/de/tum/workflows/MainLTL.scala
src/main/scala/de/tum/workflows/MainLTL.scala
+1
-1
src/main/scala/de/tum/workflows/Preconditions.scala
src/main/scala/de/tum/workflows/Preconditions.scala
+32
-23
src/main/scala/de/tum/workflows/Utils.scala
src/main/scala/de/tum/workflows/Utils.scala
+7
-3
src/main/scala/de/tum/workflows/WorkflowParser.scala
src/main/scala/de/tum/workflows/WorkflowParser.scala
+15
-11
src/main/scala/de/tum/workflows/blocks/Workflow.scala
src/main/scala/de/tum/workflows/blocks/Workflow.scala
+40
-38
src/main/scala/de/tum/workflows/foltl/FOLTL.scala
src/main/scala/de/tum/workflows/foltl/FOLTL.scala
+44
-45
src/main/scala/de/tum/workflows/foltl/FOTransformers.scala
src/main/scala/de/tum/workflows/foltl/FOTransformers.scala
+1
-0
src/main/scala/de/tum/workflows/toz3/InvariantChecker.scala
src/main/scala/de/tum/workflows/toz3/InvariantChecker.scala
+10
-9
src/main/scala/de/tum/workflows/toz3/Z3BSFO.scala
src/main/scala/de/tum/workflows/toz3/Z3BSFO.scala
+3
-2
src/test/scala/de/tum/workflows/tests/EncodingTest.scala
src/test/scala/de/tum/workflows/tests/EncodingTest.scala
+6
-6
src/test/scala/de/tum/workflows/tests/InferenceTests.scala
src/test/scala/de/tum/workflows/tests/InferenceTests.scala
+10
-0
src/test/scala/de/tum/workflows/tests/ParserTest.scala
src/test/scala/de/tum/workflows/tests/ParserTest.scala
+6
-4
src/test/scala/de/tum/workflows/tests/Z3LTLTest.scala
src/test/scala/de/tum/workflows/tests/Z3LTLTest.scala
+1
-1
src/test/scala/de/tum/workflows/tests/papertests/LeaderElectionTest.scala
...e/tum/workflows/tests/papertests/LeaderElectionTest.scala
+95
-0
No files found.
src/main/scala/de/tum/workflows/MainLTL.scala
View file @
14b736c7
...
...
@@ -32,7 +32,7 @@ object MainLTL extends App with LazyLogging {
logger
.
info
(
"Embedding FOLTL formula in LTL"
)
val
(
agents
,
res
)
=
FOTransformers
.
eliminateExistentials
(
prop
)
val
universe
=
agents
.
map
(
_
.
withType
()
).
mkString
(
", "
)
val
universe
=
agents
.
map
(
_
.
withType
).
mkString
(
", "
)
logger
.
info
(
s
"Using universe $universe"
)
if
(
agents
.
groupBy
(
_
.
typ
).
exists
(
_
.
_2
.
size
>
MAX_AGENTS
))
{
...
...
src/main/scala/de/tum/workflows/Preconditions.scala
View file @
14b736c7
...
...
@@ -18,10 +18,10 @@ object Preconditions extends LazyLogging {
for
(
s
<-
b
.
steps
)
yield
{
val
first
=
s
.
tuple
.
head
val
inner
=
if
(
first
.
typ
==
spec
.
target
.
params
.
head
.
typ
)
{
val
inf
=
Fun
(
INFNAME
,
List
(
b
.
agents
.
head
))
if
(
properties
.
stubborn
)
{
choice
.
in
(
T1
)
}
else
{
val
inf
=
Fun
(
INFNAME
,
List
(
b
.
agents
.
head
))
Or
(
And
(
Neg
(
inf
.
in
(
T1
)),
choice
.
in
(
T1
)),
And
(
inf
.
in
(
T1
),
choice
))
}
}
else
{
...
...
@@ -34,16 +34,23 @@ object Preconditions extends LazyLogging {
b
.
steps
}
val
newsteps
=
for
(
val
newb
=
b
.
updateSteps
(
guardfix
)
// for causality, add informedness updates
if
(
properties
.
stubborn
)
{
List
(
newb
)
}
else
{
val
newsteps
=
for
(
stmt
<-
b
.
steps
if
spec
.
causals
.
map
(
_
.
typ
).
contains
(
stmt
.
tuple
.
head
.
typ
)
||
stmt
.
tuple
.
head
.
typ
==
spec
.
target
.
params
.
head
.
typ
)
yield
{
val
fun
=
Fun
(
stmt
.
fun
,
stmt
.
tuple
)
// TODO
val
guard
=
Neg
(
Equiv
(
fun
.
in
(
T1
),
fun
.
in
(
T2
)))
ForallBlock
(
stmt
.
tuple
,
List
(
Add
(
guard
,
INFNAME
,
List
(
stmt
.
tuple
.
head
))))
val
fun
=
Fun
(
stmt
.
fun
,
stmt
.
tuple
)
// TODO
val
guard
=
Neg
(
Equiv
(
fun
.
in
(
T1
),
fun
.
in
(
T2
)))
ForallBlock
(
stmt
.
tuple
,
List
(
Add
(
guard
,
INFNAME
,
List
(
stmt
.
tuple
.
head
))))
}
newb
::
newsteps
}
b
::
newsteps
}
// For oracly blocks, remove O from guard and add to ForallMay choice predicate
...
...
@@ -54,7 +61,7 @@ object Preconditions extends LazyLogging {
def
findOracle
(
f
:
Formula
)
=
{
f
.
collect
{
case
f
:
Fun
if
(
f.isOracle
())
=>
List
(
f
.
name
)
case
f
:
Fun
if
f.isOracle
=>
List
(
f
.
name
)
}
}
val
oracles
=
findOracle
(
stmt
.
guard
)
...
...
@@ -68,10 +75,10 @@ object Preconditions extends LazyLogging {
def
fixguard
(
f
:
Formula
,
choice
:
Fun
)
=
{
val
nooracles
=
f
.
everywhere
{
case
f
:
Fun
if
f.isOracle
()
=>
True
case
f
:
Fun
if
f.isOracle
=>
True
}
val
decl
=
spec
.
declass
.
getOrElse
(
b
.
pred
.
get
,
(
List
(),
False
)).
_2
val
decl
=
spec
.
declass
.
getOrElse
(
name
,
(
List
(),
False
)).
_2
// FIXME: substitutions?
// FIXME: decl in T2?
And
(
nooracles
,
Or
(
And
(
decl
.
in
(
T1
),
choice
.
in
(
T1
)),
And
(
Neg
(
decl
.
in
(
T1
)),
choice
)))
...
...
@@ -86,7 +93,7 @@ object Preconditions extends LazyLogging {
}
else
b
}
def
subst
(
f
:
Formula
,
updates
:
List
[(
String
,
(
List
[
FOLTL.Var
]
,
FOLTL.Formula
))],
b
:
SimpleBlock
)
=
{
def
subst
(
f
:
Formula
,
updates
:
List
[(
String
,
(
List
[
FOLTL.Var
]
,
FOLTL.Formula
))],
b
:
SimpleBlock
)
:
Formula
=
{
updates
.
foldRight
(
f
)((
update
,
f
)
=>
{
val
(
repname
,
(
vars
,
form
))
=
update
...
...
@@ -105,7 +112,7 @@ object Preconditions extends LazyLogging {
})
}
def
getUpdate
(
s
:
Statement
,
choice
:
Option
[
Fun
],
spec
:
NISpec
,
properties
:
InvProperties
)
=
{
def
getUpdate
(
s
:
Statement
,
spec
:
NISpec
,
properties
:
InvProperties
)
:
Formula
=
{
val
frees
=
s
.
guard
.
freeVars
--
s
.
tuple
.
toSet
--
spec
.
constants
...
...
@@ -120,12 +127,12 @@ object Preconditions extends LazyLogging {
form
}
def
elaborate
(
block
:
SimpleBlock
,
spec
:
NISpec
,
properties
:
InvProperties
)
=
{
val
stepOne
=
if
(!
properties
.
stubborn
)
elaborateSteps
(
block
,
spec
,
properties
)
else
List
(
block
)
def
elaborate
(
block
:
SimpleBlock
,
spec
:
NISpec
,
properties
:
InvProperties
)
:
List
[
SimpleBlock
]
=
{
val
stepOne
=
elaborateSteps
(
block
,
spec
,
properties
)
stepOne
map
{
b
=>
elaborateOraclyBlock
(
b
,
spec
)
}
}
def
weakestPrecondition
(
post
:
Formula
,
outerb
:
SimpleBlock
,
spec
:
NISpec
,
properties
:
InvProperties
)
=
{
def
weakestPrecondition
(
post
:
Formula
,
outerb
:
SimpleBlock
,
spec
:
NISpec
,
properties
:
InvProperties
)
:
Formula
=
{
// TODO: Make 2-trace elaboration optional
...
...
@@ -138,11 +145,11 @@ object Preconditions extends LazyLogging {
precond
}
private
def
weakestPreconditionSingle
(
f
:
Formula
,
b
:
SimpleBlock
,
spec
:
NISpec
,
properties
:
InvProperties
)
=
{
private
def
weakestPreconditionSingle
(
f
:
Formula
,
b
:
SimpleBlock
,
spec
:
NISpec
,
properties
:
InvProperties
)
=
{
val
updates
=
for
(
s
<-
b
.
steps
)
yield
{
s
.
fun
->
(
s
.
tuple
,
{
getUpdate
(
s
,
b
,
spec
,
properties
)
getUpdate
(
s
,
spec
,
properties
)
})
}
...
...
@@ -152,18 +159,20 @@ 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"
)
val
neg1
=
replaced
.
toNegNf
val
neg2
=
removed
.
toNegNf
if
(
FormulaFunctions
.
collectQuantifiers
(
neg1
)
!=
FormulaFunctions
.
collectQuantifiers
(
neg2
))
{
logger
.
warn
(
s
"Would have removed a quantifier:\nBefore: ${neg1}\nAfter: $neg2"
)
}
}
re
mov
ed
re
plac
ed
}
def
abstractedPrecondition
(
f
:
Formula
,
b
:
SimpleBlock
,
spec
:
NISpec
,
properties
:
InvProperties
,
untouched
:
Set
[
String
])
=
{
def
abstractedPrecondition
(
f
:
Formula
,
b
:
SimpleBlock
,
spec
:
NISpec
,
properties
:
InvProperties
,
untouched
:
Set
[
String
])
:
Formula
=
{
val
precond
=
weakestPrecondition
(
f
,
b
,
spec
,
properties
)
// Assume untoucheds empty
// Assume untouched
predicate
s empty
val
untouchedprecond
=
precond
.
assumeEmpty
(
untouched
.
toList
)
val
z3simpednewinv
=
Z3BSFO
.
simplifyBS
(
untouchedprecond
)
...
...
@@ -179,7 +188,7 @@ object Preconditions extends LazyLogging {
// Abstract away inner existentials
val
universalinv
=
if
(
removedannotations
.
toNegNf
.
hasSubFormula
{
case
e
:
Exists
=>
true
case
_
:
Exists
=>
true
})
{
FOTransformers
.
abstractExistentials
(
removedannotations
)
}
else
{
...
...
src/main/scala/de/tum/workflows/Utils.scala
View file @
14b736c7
...
...
@@ -5,8 +5,7 @@ import de.tum.workflows.foltl.FOLTL._
import
java.io.File
import
java.io.PrintWriter
import
de.tum.workflows.toz3.InvariantChecker
import
de.tum.workflows.toz3.InvProperties
import
de.tum.workflows.toz3.
{
InvProperties
,
InvariantChecker
,
Z3BSFO
}
import
com.typesafe.scalalogging.LazyLogging
import
de.tum.workflows.MainInvariantsInference.logger
...
...
@@ -74,13 +73,18 @@ object Utils extends LazyLogging {
val
basename
=
name
.
split
(
"/"
).
last
val
filenames
=
s
"${basename}_$model${if (desc.isEmpty()) "" else s"
_$desc
"}"
// do not blow up the formula with auxilliary elimination
val
(
res
,
graph
,
labelling
,
provens
,
dot
,
time
)
=
InvariantChecker
.
checkInvariantFPLabelling
(
spec
,
inv
,
properties
)
logger
.
info
(
s
"Invariant was ${inv}"
)
logger
.
info
(
s
"Invariant was ${if (res) "" else "
not
"}proven (took $time ms)\n"
)
if
(!
res
)
{
val
headinv
=
labelling
.
last
(
graph
.
nodes
.
head
)
val
satq
=
And
(
spec
.
always
,
Neg
(
headinv
))
logger
.
info
(
s
"Initial state violating the invariant: ${Z3BSFO.debugmodelBS(satq)}"
)
}
for
((
s
,
i
)
<-
dot
.
zipWithIndex
)
{
Utils
.
write
(
name
,
s
"${filenames}_$i.dot"
,
s
)
}
...
...
src/main/scala/de/tum/workflows/WorkflowParser.scala
View file @
14b736c7
...
...
@@ -76,15 +76,16 @@ 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
)
toSet
val
oracles
=
filtered
.
filter
(
_
.
isOracle
())
val
bs
=
filtered
.
filter
(
_
.
isB
())
val
rels
=
filtered
--
oracles
--
bs
Signature
(
oracles
,
bs
,
rels
)
val
filtered
=
preds
.
groupBy
(
_
.
name
).
map
(
_
.
_2
.
head
).
toSet
val
oracles
=
filtered
.
filter
(
_
.
isOracle
)
val
constinputs
=
filtered
.
filter
(
_
.
isConstInput
)
val
bs
=
filtered
.
filter
(
_
.
isB
)
val
rels
=
filtered
--
oracles
--
constinputs
--
bs
Signature
(
oracles
,
constinputs
,
bs
,
rels
)
}
def
typeMap
(
typedvars
:
List
[
Var
])
=
{
typedvars
.
map
(
v
=>
v
.
name
->
v
.
typ
)
toMap
typedvars
.
map
(
v
=>
v
.
name
->
v
.
typ
)
.
toMap
}
def
inferType
(
typemap
:
Map
[
String
,
String
],
v
:
Var
)
=
{
...
...
@@ -136,13 +137,15 @@ object WorkflowParser extends RegexParsers with PackratParsers with LazyLogging
def
TUPLE
=
"("
~>
repsep
(
TYPEDVAR
,
","
)
<~
")"
def
FUN
=
VAR
~
TUPLE
^^
{
case
f
~
tup
=>
Fun
(
f
.
name
,
tup
)
}
def
EQ
=
(
VAR
<~
"="
)
~
VAR
^^
{
case
v1
~
v2
=>
Equal
(
v1
,
v2
)
}
|
(
VAR
<~
"≠"
)
~
VAR
^^
{
case
v1
~
v2
=>
Neg
(
Equal
(
v1
,
v2
))
}
def
EQUIV
=
"("
~>
(
SIMPLETERM
<~
"<->"
)
~
(
TERM
<~
")"
)
^^
{
case
t1
~
t2
=>
Equiv
(
t1
,
t2
)
}
def
EXISTS
=
"∃"
~>
(
repsep
(
TYPEDVAR
,
","
)
<~
(
"."
?))
~
TERM
^^
{
case
vs
~
t
=>
Exists
(
vs
,
t
)
}
def
FORALL
=
"∀"
~>
(
repsep
(
TYPEDVAR
,
","
)
<~
(
"."
?))
~
TERM
^^
{
case
vs
~
t
=>
Forall
(
vs
,
t
)
}
def
QUANTIFIER
=
EXISTS
|
FORALL
def
QUANTIFIER
:
PackratParser
[
Formula
]
=
EXISTS
|
FORALL
def
SIMPLETERM
=
(
tt
|
ff
|
FUN
)
lazy
val
TERM
:
PackratParser
[
Formula
]
=
(
AND
|
OR
|
IMPLIES
|
NEG
|
SIMPLETERM
|
GLOBALLY
|
FINALLY
|
QUANTIFIER
)
def
SIMPLETERM
=
tt
|
ff
|
FUN
|
EQ
lazy
val
TERM
:
PackratParser
[
Formula
]
=
AND
|
OR
|
IMPLIES
|
NEG
|
SIMPLETERM
|
GLOBALLY
|
FINALLY
|
QUANTIFIER
|
EQUIV
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
)
}
...
...
@@ -154,7 +157,8 @@ object WorkflowParser extends RegexParsers with PackratParsers with LazyLogging
def
BLOCK
=
"forall"
~>
(
"may"
?)
~
repsep
(
TYPEDVAR
,
","
)
~
(
STMT
+)
^?
({
// all free variables contained
case
may
~
vars
~
stmts
if
validblock
(
vars
,
stmts
)
=>
{
val
typemap
=
typeMap
(
vars
)
// add quantified variables to typemap
val
typemap
=
typeMap
(
vars
++
stmts
.
flatMap
(
_
.
guard
.
boundVars
))
val
typedstmts
=
stmts
map
(
inferTypes
(
typemap
,
_
))
if
(
may
.
isEmpty
)
{
ForallBlock
(
vars
,
typedstmts
)
...
...
@@ -186,7 +190,7 @@ object WorkflowParser extends RegexParsers with PackratParsers with LazyLogging
((
"Declassify"
~>
DECLASS
)?)
~
(
"Target"
~>
FUN
)
~
((
"Causality"
~>
repsep
(
TYPEDVAR
,
","
))?)
^^
{
case
_
~
w
~
decl
~
tar
~
causals
=>
NISpec
(
w
,
toMap
(
decl
.
toList
),
tar
,
causals
.
getOrElse
(
List
()))
case
_
~
w
~
decl
~
tar
~
causals
=>
NISpec
(
w
,
toMap
(
decl
.
toList
),
True
,
tar
,
causals
.
getOrElse
(
List
()))
}
def
toMap
(
list
:
List
[(
Fun
,
Formula
)])
:
Map
[
String
,
(
List
[
Var
]
,
Formula
)]
=
{
...
...
src/main/scala/de/tum/workflows/blocks/Workflow.scala
View file @
14b736c7
...
...
@@ -11,8 +11,8 @@ object Signature {
}
case
class
Workflow
(
sig
:
Signature
,
steps
:
List
[
Block
])
{
override
def
toString
()
=
steps
.
mkString
(
"\n"
)
lazy
val
isomitting
=
{
override
def
toString
()
:
String
=
steps
.
mkString
(
"\n"
)
lazy
val
isomitting
:
Boolean
=
{
steps
.
exists
(
_
.
isomitting
)
}
}
...
...
@@ -24,18 +24,8 @@ trait Spec {
def
w
:
Workflow
}
case
class
InvSpec
(
w
:
Workflow
,
always
:
Formula
,
invariant
:
Formula
)
extends
Spec
{
override
def
toString
=
{
s
"Spec\nWorkflow:\n$w\nAlways:$always\nInvariant:$invariant"
}
def
toNISpec
()
=
{
NISpec
(
w
,
Map
(),
Fun
(
"NOTHING"
,
List
()),
List
())
}
}
case
class
NISpec
(
w
:
Workflow
,
declass
:
Map
[
String
,
(
List
[
Var
]
,
Formula
)],
target
:
Fun
,
causals
:
List
[
Var
])
extends
Spec
with
LazyLogging
{
override
def
toString
=
{
case
class
NISpec
(
w
:
Workflow
,
declass
:
Map
[
String
,
(
List
[
Var
]
,
Formula
)],
always
:
Formula
,
target
:
Fun
,
causals
:
List
[
Var
])
extends
Spec
with
LazyLogging
{
override
def
toString
:
String
=
{
s
"NISpec\nWorkflow:\n$w\nDeclass:$declass\nTarget:$target"
}
...
...
@@ -47,7 +37,7 @@ case class NISpec(w: Workflow, declass: Map[String, (List[Var], Formula)], targe
// TODO: How to check for more constants?
}
def
checkSanity
()
=
{
def
checkSanity
()
:
Boolean
=
{
var
sane
=
true
// TODO: check all types
...
...
@@ -65,18 +55,18 @@ case class NISpec(w: Workflow, declass: Map[String, (List[Var], Formula)], targe
// Oracle only positive
val
f
=
stmt
.
guard
.
toNegNf
val
noneg
=
!
f
.
hasSubFormula
{
case
Neg
(
f
:
Fun
)
if
f
.
isOracle
()
=>
true
case
Neg
(
f
:
Fun
)
if
f
.
isOracle
=>
true
}
if
(!
noneg
)
{
logger
.
error
(
s
"Found negated oracle in guard for statement $stmt"
)
}
val
allvars
=
!(
f
hasSubFormula
{
case
f
:
Fun
if
f.isOracle
&&
f.params
!=
frees
=>
true
})
if
(!
allvars
)
{
logger
.
error
(
s
"Found oracle with wrong parameters in statement $stmt"
)
}
noneg
&&
allvars
//
val allvars = !(f hasSubFormula {
//
case f:Fun if f.isOracle && f.params != frees => true
//
})
//
if (!allvars) {
//
logger.error(s"Found oracle with wrong parameters in statement $stmt")
//
}
noneg
//
&& allvars
}
// check same relation only updated once per block
...
...
@@ -103,9 +93,13 @@ case class NISpec(w: Workflow, declass: Map[String, (List[Var], Formula)], targe
sane
&&=
isSane
(
w
.
steps
)
sane
}
def
addKnowledge
(
k
:
Formula
)
=
{
NISpec
(
w
,
declass
,
And
.
make
(
always
,
k
),
target
,
causals
)
}
}
object
NISpec
{
val
EMPTY
=
NISpec
(
Workflow
.
EMPTY
,
Map
(),
Fun
(
"NOTHING"
,
List
()),
List
())
val
EMPTY
=
NISpec
(
Workflow
.
EMPTY
,
Map
(),
True
,
Fun
(
"NOTHING"
,
List
()),
List
())
}
abstract
sealed
class
Block
{
...
...
@@ -113,13 +107,15 @@ abstract sealed class Block {
}
abstract
sealed
class
SimpleBlock
extends
Block
{
type
This
>:
this.
type
<:
SimpleBlock
def
agents
:
List
[
Var
]
def
steps
:
List
[
Statement
]
def
may
:
Boolean
def
pred
:
Option
[
String
]
def
updateSteps
(
s
:
List
[
Statement
])
def
updateSteps
(
s
:
List
[
Statement
])
:
This
override
def
isomitting
=
{
override
def
isomitting
:
Boolean
=
{
// a simple block is omitting, if there exists a statement where not all agents appear in the tuple
steps
.
exists
(
s
=>
agents
.
exists
(
a
=>
!
s
.
tuple
.
contains
(
a
)))
}
...
...
@@ -128,11 +124,11 @@ abstract sealed class SimpleBlock extends Block {
// before transformation
val
before
=
steps
.
exists
(
s
=>
{
s
.
guard
.
hasSubFormula
{
case
f
:
Fun
=>
f
.
isOracle
()
case
f
:
Fun
=>
f
.
isOracle
}
})
// after transformation
val
after
=
pred
.
exists
(
name
=>
Fun
(
name
,
agents
).
isOracle
()
)
val
after
=
pred
.
exists
(
name
=>
Fun
(
name
,
agents
).
isOracle
)
before
||
after
}
...
...
@@ -150,50 +146,56 @@ abstract sealed class SimpleBlock extends Block {
}
abstract
class
Statement
{
type
This
>:
this.
type
<:
Statement
def
guard
:
Formula
def
fun
:
String
def
tuple
:
List
[
Var
]
def
updateGuard
(
newguard
:
Formula
)
def
updateGuard
(
newguard
:
Formula
)
:
This
lazy
val
freeVars
=
guard
.
freeVars
++
tuple
lazy
val
freeVars
:
Set
[
Var
]
=
guard
.
freeVars
++
tuple
}
case
class
Add
(
guard
:
Formula
,
fun
:
String
,
tuple
:
List
[
Var
])
extends
Statement
{
override
def
toString
()
=
guard
+
" → "
+
fun
+
" += "
+
tuple
.
mkString
(
"("
,
","
,
")"
)
+
";"
type
This
=
Add
override
def
toString
()
:
String
=
guard
+
" → "
+
fun
+
" += "
+
tuple
.
mkString
(
"("
,
","
,
")"
)
+
";"
override
def
updateGuard
(
newguard
:
Formula
)
=
Add
(
newguard
,
fun
,
tuple
)
}
case
class
Remove
(
guard
:
Formula
,
fun
:
String
,
tuple
:
List
[
Var
])
extends
Statement
{
override
def
toString
()
=
guard
+
" → "
+
fun
+
" -= "
+
tuple
.
mkString
(
"("
,
","
,
")"
)
+
";"
type
This
=
Remove
override
def
toString
()
:
String
=
guard
+
" → "
+
fun
+
" -= "
+
tuple
.
mkString
(
"("
,
","
,
")"
)
+
";"
override
def
updateGuard
(
newguard
:
Formula
)
=
Remove
(
newguard
,
fun
,
tuple
)
}
case
class
ForallBlock
(
agents
:
List
[
Var
],
steps
:
List
[
Statement
])
extends
SimpleBlock
{
type
This
=
ForallBlock
val
may
=
false
override
def
toString
()
=
"forall "
+
agents
.
map
(
_
.
withType
).
mkString
(
","
)
+
steps
.
mkString
(
"\n "
,
"\n "
,
""
)
override
def
pred
()
=
None
override
def
toString
()
:
String
=
"forall "
+
agents
.
map
(
_
.
withType
).
mkString
(
","
)
+
steps
.
mkString
(
"\n "
,
"\n "
,
""
)
override
def
updateSteps
(
newsteps
:
List
[
Statement
])
=
ForallBlock
(
agents
,
newsteps
)
}
case
class
ForallMayBlock
(
agents
:
List
[
Var
],
choice
:
String
,
steps
:
List
[
Statement
])
extends
SimpleBlock
{
type
This
=
ForallMayBlock
val
may
=
true
override
def
toString
()
=
"forall "
+
agents
.
map
(
_
.
withType
).
mkString
(
","
)
+
" may ("
+
pred
+
")"
+
steps
.
mkString
(
"\n "
,
"\n "
,
""
)
override
def
pred
()
=
Some
(
choice
)
override
def
toString
()
:
String
=
"forall "
+
agents
.
map
(
_
.
withType
).
mkString
(
","
)
+
" may ("
+
pred
+
")"
+
steps
.
mkString
(
"\n "
,
"\n "
,
""
)
override
def
updateSteps
(
newsteps
:
List
[
Statement
])
=
ForallMayBlock
(
agents
,
choice
,
newsteps
)
}
case
class
Loop
(
steps
:
List
[
Block
])
extends
Block
{
override
def
toString
()
=
{
override
def
toString
()
:
String
=
{
// indentation
"loop(*)\n"
+
Utils
.
indentLines
(
steps
.
mkString
(
"\n"
))
}
override
def
isomitting
=
{
override
def
isomitting
:
Boolean
=
{
steps
.
exists
(
_
.
isomitting
)
}
}
case
class
NondetChoice
(
left
:
List
[
Block
],
right
:
List
[
Block
])
extends
Block
{
override
def
toString
()
=
{
override
def
toString
()
:
String
=
{
"choose {\n"
+
Utils
.
indentLines
(
left
.
mkString
(
"\n"
))
+
"\n} {\n"
+
Utils
.
indentLines
(
right
.
mkString
(
"\n"
))
+
"\n}\n"
}
override
def
isomitting
=
{
override
def
isomitting
:
Boolean
=
{
left
.
exists
(
_
.
isomitting
)
||
right
.
exists
(
_
.
isomitting
)
}
}
src/main/scala/de/tum/workflows/foltl/FOLTL.scala
View file @
14b736c7
package
de.tum.workflows.foltl
import
de.tum.workflows.Utils
import
de.tum.workflows.foltl.FOLTL.FunFromVar
import
de.tum.workflows.foltl.FOLTL.FunFromVar.getVars
import
scala.
annotation.tailrec
import
scala.
util.matching.Regex
//import de.tum.workflows.foltl.TermFunctions._
...
...
@@ -37,7 +35,7 @@ object FOLTL {
lazy
val
bracketed
:
String
=
this
match
{
case
_:
BinOp
=>
"("
+
this
+
")"
case
_
=>
this
.
toString
()
case
_
=>
this
.
toString
}
// single arrow is for maps
...
...
@@ -80,15 +78,15 @@ object FOLTL {
val
DEFAULT_TYPE
=
"T"
}
case
class
Var
(
name
:
String
,
typ
:
String
=
Var
.
DEFAULT_TYPE
)
extends
Formula
{
override
def
toString
()
=
s
"$name"
def
withType
()
=
s
"$name:$typ"
override
def
toString
=
s
"$name"
def
withType
=
s
"$name:$typ"
}
object
Fun
{
def
apply
(
name
:
String
,
params
:
List
[
Var
])
:
Fun
=
Fun
(
name
,
None
,
params
)
}
object
FunNameFromVar
{
val
PredicateNoParam
=
"([a-zA-Z0-9]+)(#([a-zA-Z0-9]+))?"
.
r
val
PredicateNoParam
:
Regex
=
"([a-zA-Z0-9]+)(#([a-zA-Z0-9]+))?"
.
r
def
unapply
(
s
:
String
)
:
Option
[(
String
,
Option
[
String
])]
=
{
s
match
{
...
...
@@ -99,15 +97,15 @@ object FOLTL {
}
}
object
FunFromVar
{
val
Predicate
=
"([a-zA-Z0-9]+)(#([a-zA-Z0-9]+))?((_[a-zA-Z0-9]+#[a-zA-Z0-9]+)*)"
.
r
val
Predicate
:
Regex
=
"([a-zA-Z0-9]+)(#([a-zA-Z0-9]+))?((_[a-zA-Z0-9]+#[a-zA-Z0-9]+)*)"
.
r
def
getVars
(
s
:
String
)
=
{
val
split
=
s
split
(
"_"
)
def
getVars
(
s
:
String
)
:
List
[
Var
]
=
{
val
split
=
s
split
"_"
if
(
split
.
length
>
1
)
{
split
.
drop
(
1
).
map
(
str
=>
{
val
Array
(
name
,
typ
)
=
str
.
split
(
"#"
)
Var
(
name
,
typ
)
})
toList
})
.
toList
}
else
{
List
()
}
...
...
@@ -123,20 +121,21 @@ object FOLTL {
}
case
class
Fun
(
name
:
String
,
ind
:
Option
[
String
],
params
:
List
[
Var
])
extends
Formula
{
override
def
toString
()
=
name
+
Utils
.
mkString
(
ind
,
"("
,
""
,
")"
)
+
params
.
map
(
_
.
name
).
mkString
(
"("
,
","
,
")"
)
override
def
toString
:
String
=
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
)
def
isOracle
()
=
name
.
startsWith
(
"O"
)
def
isAux
()
=
name
.
startsWith
(
"choice"
)
def
isB
()
=
name
.
startsWith
(
"B"
)
def
isOracle
:
Boolean
=
name
.
startsWith
(
"O"
)
def
isConstInput
:
Boolean
=
name
.
startsWith
(
"I"
)
def
isAux
:
Boolean
=
name
.
startsWith
(
"choice"
)
def
isB
:
Boolean
=
name
.
startsWith
(
"B"
)
def
encodeToVar
()
=
{
def
encodeToVar
()
:
Var
=
{
val
pi
=
if
(
ind
.
isDefined
)
"#"
+
ind
.
get
else
""
val
tup
=
params
.
map
(
p
=>
p
.
name
+
"#"
+
p
.
typ
)
Var
(
name
+
pi
+
Utils
.
mkString
(
tup
,
"_"
,
"_"
,
""
))
}
def
encodeName
()
=
{
def
encodeName
()
:
String
=
{
val
pi
=
if
(
ind
.
isDefined
)
"#"
+
ind
.
get
else
""
name
+
pi
}
...
...
@@ -148,26 +147,26 @@ object FOLTL {
def
vars
:
List
[
Var
]
def
t
:
Formula
override
def
toString
()
=
{
override
def
toString
:
String
=
{
// show types only in quantifiers
qname
+
" "
+
vars
.
map
(
_
.
withType
()
).
mkString
(
","
)
+
". "
+
t
.
bracketed
qname
+
" "
+
vars
.
map
(
_
.
withType
).
mkString
(
","
)
+
". "
+
t
.
bracketed
}
}
object
Quantifier
{
def
unapply
(
q
:
Quantifier
)
=
Some
((
q
.
make
,
q
.
vars
,
q
.
t
))
def
make
(
m
:
(
List
[
Var
],
Formula
)
=>
Quantifier
,
l
:
List
[
Var
],
f
:
Formula
)
=
{
def
make
(
m
:
(
List
[
Var
],
Formula
)
=>
Quantifier
,
l
:
List
[
Var
],
f
:
Formula
)
:
Formula
=
{
if
(
l
.
isEmpty
)
f
else
m
(
l
,
f
)
}
}
object
Exists
{
def
make
=
Quantifier
.
make
(
Exists
.
apply
,
_:
List
[
Var
],
_:
Formula
)
def
make
:
(
List
[
Var
],
Formula
)
=>
Formula
=
Quantifier
.
make
(
Exists
.
apply
,
_:
List
[
Var
],
_:
Formula
)
}
object
Forall
{
def
make
=
Quantifier
.
make
(
Forall
.
apply
,
_:
List
[
Var
],
_:
Formula
)
def
make
:
(
List
[
Var
],
Formula
)
=>
Formula
=
Quantifier
.
make
(
Forall
.
apply
,
_:
List
[
Var
],
_:
Formula
)
}
object
ForallOtherThan
{
def
make
(
l
:
List
[
Var
],
otherthan
:
List
[
Var
],
f
:
Formula
)
=
{
def
make
(
l
:
List
[
Var
],
otherthan
:
List
[
Var
],
f
:
Formula
)
:
Formula
=
{
if
(
otherthan
.
isEmpty
||
l
.
isEmpty
)
{
Forall
.
make
(
l
,
f
)
}
else
{
ForallOtherThan
(
l
,
otherthan
,
f
)
}
...
...
@@ -175,17 +174,17 @@ object FOLTL {
}
case
class
Exists
(
vars
:
List
[
Var
],
t
:
Formula
)
extends
Quantifier
{
val
qname
=
"∃"
val
make
=
Quantifier
.
make
(
Exists
.
apply
,
_
,
_
)
val
make
:
(
List
[
Var
],
Formula
)
=>
Formula
=
Quantifier
.
make
(
Exists
.
apply
,
_
,
_
)
}
case
class
Forall
(
vars
:
List
[
Var
],
t
:
Formula
)
extends
Quantifier
{
val
qname
=
"∀"
val
make
=
Quantifier
.
make
(
Forall
.
apply
,
_
,
_
)
val
make
:
(
List
[
Var
],
Formula
)
=>
Formula
=
Quantifier
.
make
(
Forall
.
apply
,
_
,
_
)
}
case
class
ForallOtherThan
(
vars
:
List
[
Var
],
otherthan
:
List
[
Var
],
t
:
Formula
)
extends
Quantifier
{
val
qname
=
"∀"
val
make
=
ForallOtherThan
.
apply
(
_:
List
[
Var
],
otherthan
,
_:
Formula
)
override
def
toString
()
=
{
s
"$qname ${vars.map(_.withType
()).mkString("
,
")} ∉ {${otherthan.map(_.withType()
).mkString("
,
")}}. ${t.bracketed}"
override
def
toString
:
String
=
{
s
"$qname ${vars.map(_.withType
).mkString("
,
")} ∉ {${otherthan.map(_.withType
).mkString("
,
")}}. ${t.bracketed}"
}
}
...
...
@@ -219,11 +218,11 @@ object FOLTL {
def
opname
:
String
def
t
:
Formula
override
def
toString
()
=
opname
+
" "
+
t
.
bracketed
override
def
toString
:
String
=
opname
+
" "
+
t
.
bracketed
}
object
UnOp
{
def
unapply
(
unop
:
UnOp
)
=
{
def
unapply
(
unop
:
UnOp
)
:
Some
[(
Formula
=>
UnOp
,
Formula
)]
=
{
Some
((
unop
.
make
,
unop
.
t
))
}
}
...
...
@@ -234,22 +233,22 @@ object FOLTL {
def
t1
:
Formula
def
t2
:
Formula
override
def
toString
()
=
{
override
def
toString
:
String
=
{
(
t1
,
t2
)
match
{
case
(
t1
:
BinOp
,
t2
:
BinOp
)
if
(
opname
==
t1
.
opname
&&
opname
==
t2
.
opname
)
=>
t1
+
" "
+
opname
+
" "
+
t2
case
(
t1
:
BinOp
,
_
)
if
(
opname
==
t1
.
opname
)
=>
t1
+
" "
+
opname
+
" "
+
t2
.
bracketed
case
(
_
,
t2
:
BinOp
)
if
(
opname
==
t2
.
opname
)
=>
t1
.
bracketed
+
" "
+
opname
+
" "
+
t2
case
(
t1
:
BinOp
,
t2
:
BinOp
)
if
opname
==
t1
.
opname
&&
opname
==
t2
.
opname
=>
t1
+
" "
+
opname
+
" "
+
t2
case
(
t1
:
BinOp
,
_
)
if
opname
==
t1
.
opname
=>
t1
+
" "
+
opname
+
" "
+
t2
.
bracketed
case
(
_
,
t2
:
BinOp
)
if
opname
==
t2
.
opname
=>
t1
.
bracketed
+
" "
+
opname
+
" "
+
t2
case
_
=>
t1
.
bracketed
+
" "
+
opname
+
" "
+
t2
.
bracketed
}
}
}
object
BinOp
{
def
unapply
(
binop
:
BinOp
)
=
{
def
unapply
(
binop
:
BinOp
)
:
Some
[((
Formula
,
Formula
)
=>
BinOp
,
Formula
,
Formula
)]
=
{
Some
((
binop
.
make
,
binop
.
t1
,
binop
.
t2
))
}
// TODO: make tail-recursive list lefthanging?
// TODO: make tail-recursive list left
hanging?
// @tailrec
// def makeL(make: (Formula, Formula) => Formula, l: Seq[Formula], Empty: Formula, acc:Formula): Formula = {
// l.toList match {
...
...
@@ -275,10 +274,10 @@ object FOLTL {
}
object
Or
{
def
make
(
terms
:
List
[
Formula
])
=
{
def
make
(
terms
:
List
[
Formula
])
:
Formula
=
{
BinOp
.
makeL
(
Or
.
apply
,
terms
,
False
)
}
def
make
(
terms
:
Formula*
)
=
{
def
make
(
terms
:
Formula*
)
:
Formula
=
{
BinOp
.
makeL
(
Or
.
apply
,
terms
,
False
)
}
}
...
...
@@ -289,10 +288,10 @@ object FOLTL {
}
object
And
{
def
make
(
terms
:
List
[
Formula
])
=
{
def
make
(
terms
:
List
[
Formula
])
:
Formula
=
{
BinOp
.
makeL
(
And
.
apply
,
terms
,
True
)
}
def
make
(
terms
:
Formula*
)
=
{
def
make
(
terms
:
Formula*
)
:
Formula
=
{
BinOp
.
makeL
(
And
.
apply
,
terms
,
True
)
}
}
...
...
@@ -307,10 +306,10 @@ object FOLTL {
val
make
=
Equiv
.
apply
}
object
Equiv
{
def
make
(
terms
:
List
[
Formula
])
=
{
def
make
(
terms
:
List
[
Formula
])
:
Formula
=
{
BinOp
.
makeL
(
Equiv
.
apply
,
terms
,
True
)
}
def
make
(
terms
:
Formula*
)
=
{
def
make
(
terms
:
Formula*
)
:
Formula
=
{
BinOp
.
makeL
(
Equiv
.
apply
,
terms
,
True
)
}
}
...
...
@@ -320,10 +319,10 @@ object FOLTL {
val
make
=
Equal
.
apply
}
object
Equal
{
def
make
(
terms
:
List
[
Formula
])
=
{
def
make
(
terms
:
List
[
Formula
])
:
Formula
=
{
BinOp
.
makeL
(
Equal
.
apply
,
terms
,
True
)
}
def
make
(
terms
:
Formula*
)
=
{
def
make
(
terms
:
Formula*
)
:
Formula
=
{
BinOp
.
makeL
(
Equal
.
apply
,
terms
,
True
)
}
}
...
...
@@ -333,10 +332,10 @@ object FOLTL {
val
make
=
Implies
.
apply
}
object
Implies
{
def
make
(
terms
:
List
[
Formula
])
=
{
def
make
(
terms
:
List
[
Formula
])
:
Formula
=
{
BinOp
.
makeL
(
Implies
.
apply
,
terms
,
True
)
}
def
make
(
terms
:
Formula*
)
=
{
def
make
(
terms
:
Formula*
)
:
Formula
=
{
BinOp
.
makeL
(
Implies
.
apply
,
terms
,
True
)
}