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
9c620cdc
Commit
9c620cdc
authored
May 05, 2017
by
Christian Müller
Browse files
add twocausals, add &&,|| syntax
parent
7588f530
Changes
3
Hide whitespace changes
Inline
Side-by-side
examples/twocausals_sat.spec
0 → 100644
View file @
9c620cdc
Workflow
forallmay a
True -> T1 += (a)
forallmay a
¬ T1(a) -> T2 += (a)
forallmay a
(¬ T1(a) ∧ ¬ T2(a)) -> T3 += (a)
forall a
(O(a) ∧ T1(a)) -> R += (a)
forallmay a,b
(T1(a) ∧ T2(b)) -> S += (b, a)
forallmay a,b
(T2(a) ∧ T3(b)) -> S += (b, a)
Declassify
O(x): F (T1(x) ∨ T2(x))
Target
S(a1, a2)
Causality
ca, cb
examples/twocausals_unsat.spec
0 → 100644
View file @
9c620cdc
Workflow
forallmay a
True -> T1 += (a)
forallmay a
¬ T1(a) -> T2 += (a)
forallmay a
(¬ T1(a) ∧ ¬ T2(a)) -> T3 += (a)
forall a
(O(a) ∧ T1(a)) -> R += (a)
forallmay a,b
(T1(a) ∧ T2(b)) -> S += (b, a)
forallmay a,b
(T2(a) ∧ T3(b)) -> S += (b, a)
Declassify
O(x): F (T1(x) ∨ T2(x))
Target
S(a1, a2)
Causality
ca
src/main/scala/de/tum/workflows/WorkflowParser.scala
View file @
9c620cdc
...
...
@@ -116,9 +116,11 @@ object WorkflowParser extends RegexParsers with LazyLogging {
// logics
def
tt
=
"True"
^^^
True
def
ff
=
"False"
^^^
False
def
AND
=
repsep
(
SIMPLETERM
,
"∧"
)
^^
{
case
ts
=>
And
.
make
(
ts
)
}
def
OR
=
repsep
(
SIMPLETERM
,
"∨"
)
^^
{
case
ts
=>
Or
.
make
(
ts
)
}
def
NEG
=
(
"¬"
|
"!"
)
~
SIMPLETERM
^^
{
case
_
~
t
=>
Neg
(
t
)
}
def
AND
=
(
repsep
(
TERM
,
"∧"
)
|
repsep
(
TERM
,
"&&"
))
^^
{
case
ts
=>
And
.
make
(
ts
)
}
def
OR
=
(
repsep
(
TERM
,
"∨"
)
|
repsep
(
TERM
,
"||"
))
^^
{
case
ts
=>
Or
.
make
(
ts
)
}
def
SIMPLETERM
=
(
tt
|
ff
|
FUN
)
def
NEG
=
(
"¬"
|
"!"
)
~>
TERM
^^
{
case
t
=>
Neg
(
t
)
}
def
TERM
:
Parser
[
Term
]
=
(
SIMPLETERM
|
GLOBALLY
|
FINALLY
|
"("
~>
AND
<~
")"
|
"("
~>
OR
<~
")"
|
NEG
)
// temporals
def
GLOBALLY
=
(
"G"
|
"☐"
)
~>
TERM
^^
{
case
t
=>
Globally
(
t
)
}
...
...
@@ -127,9 +129,6 @@ object WorkflowParser extends RegexParsers with LazyLogging {
def
TUPLE
=
"("
~>
repsep
(
TYPEDVAR
,
","
)
<~
")"
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
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
)
}
...
...
Write
Preview
Supports
Markdown
0%
Try again
or
attach a new 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