Commit 49d1c9ef authored by Christian Müller's avatar Christian Müller

supersafe readme

parent e57b83c3
......@@ -22,3 +22,4 @@ project/plugins/project/
build
.classpath
.settings/
/bin/
......@@ -9,13 +9,17 @@ For now, it is possible to generate the LTL formula for a workflow using
``Encoding.toFOLTL(w)``
and translate it to pure LTL that can be parsed by Spot.
An example can be found at ``de.tum.workflows.Main``
It can be run using ``sbt run`` and logs the resulting LTL formulas for the example workflow to the console.
## Building
To get sbt to build the project properly, you have to add the Supersafe Compiler plugin by adding
``resolvers += "Artima Maven Repository" at "http://repo.artima.com/releases"`` to ``~/.sbt/0.13/global.sbt``
(You can generate an eclipse project file for use with Scala IDE by running ``sbt eclipse`` after installing the sbt plugin)
## Testing
An example can be found at ``de.tum.workflows.Main``
It can be run using ``sbt run`` and logs the resulting LTL formulas for the example workflow to the console.
Generating an accepting run can be done by locally installing Spot (https://spot.lrde.epita.fr),
or at https://spot.lrde.epita.fr/trans.html.
G (
(n0 → X n1) ∧ (n1 → X (n3 ∨ n2)) ∧ (n2 → X n2) ∧ (n3 → X n1)
) ∧ G (¬(n0 ∧ n1) ∧ ¬(n0 ∧ n2) ∧ ¬(n0 ∧ n3) ∧ ¬(n1 ∧ n2) ∧ ¬(n1 ∧ n3) ∧ ¬(n2 ∧ n3)) ∧
G (
((n0 ∧ X n1) →
((X Q_a_a ↔ (Q_a_a ∨ (O_a ∧ choice0_a_a))) ∧
) ∧ G (
¬(n0 ∧ n1) ∧ ¬(n0 ∧ n2) ∧ ¬(n0 ∧ n3) ∧ ¬(n1 ∧ n2) ∧ ¬(n1 ∧ n3) ∧ ¬(n2 ∧ n3)
) ∧ G (
((n0 ∧ X n1) → (
(X Q_a_a ↔ (Q_a_a ∨ (O_a ∧ choice0_a_a))) ∧
(X O_a ↔ O_a) ∧
(X R_a_a ↔ R_a_a) ∧
(X S_a_a_a ↔ S_a_a_a))) ∧
((n1 ∧ X n3) →
((X S_a_a_a ↔ (S_a_a_a ∨ R_a_a)) ∧
(X S_a_a_a ↔ S_a_a_a)
)) ∧
((n1 ∧ X n3) → (
(X S_a_a_a ↔ (S_a_a_a ∨ (R_a_a ∧ choice1_a_a_a))) ∧
(X O_a ↔ O_a) ∧
(X Q_a_a ↔ Q_a_a) ∧
(X R_a_a ↔ R_a_a))) ∧
((n1 ∧ X n2) →
((X O_a ↔ O_a) ∧
(X Q_a_a ↔ Q_a_a) ∧
(X R_a_a ↔ R_a_a)
)) ∧
((n1 ∧ X n2) → (
(X O_a ↔ O_a) ∧ (X Q_a_a ↔ Q_a_a) ∧
(X R_a_a ↔ R_a_a) ∧
(X S_a_a_a ↔ S_a_a_a))) ∧
((n2 ∧ X n2) →
((X O_a ↔ O_a) ∧
(X S_a_a_a ↔ S_a_a_a)
)) ∧
((n2 ∧ X n2) → (
(X O_a ↔ O_a) ∧
(X Q_a_a ↔ Q_a_a) ∧
(X R_a_a ↔ R_a_a) ∧
(X S_a_a_a ↔ S_a_a_a))) ∧
((n3 ∧ X n1) →
((X R_a_a ↔ (R_a_a ∨ Q_a_a)) ∧
(X S_a_a_a ↔ S_a_a_a)
)) ∧
((n3 ∧ X n1) → (
(X R_a_a ↔ (R_a_a ∨ Q_a_a)) ∧
(X O_a ↔ O_a) ∧
(X Q_a_a ↔ Q_a_a) ∧
(X S_a_a_a ↔ S_a_a_a)))) ∧
n0 ∧ ¬n1 ∧ ¬n2 ∧ ¬n3 ∧ ¬Q_a_a ∧ ¬R_a_a ∧ ¬S_a_a_a
(X S_a_a_a ↔ S_a_a_a)
))
) ∧ n0 ∧ ¬n1 ∧ ¬n2 ∧ ¬n3 ∧ ¬Q_a_a ∧ ¬R_a_a ∧ ¬S_a_a_a
......@@ -35,7 +35,7 @@ object Main extends App with LazyLogging {
val res = Encoding.toFOLTL(w)
// agent list to execute the workflow for (should not clash with variables in the workflow)
val agents:List[Var] = List("a","b","c")
val agents:List[Var] = List("a")
val res2 = LTL.eliminateUniversals(res, agents)
val res3 = LTL.eliminatePredicates(res2)
logger.info(s"Complete formula: $res3")
......
Markdown is supported
0% or
You are about to add 0 people to the discussion. Proceed with caution.
Finish editing this message first!
Please register or to comment