Main.scala 1019 Bytes
Newer Older
Christian Müller's avatar
Christian Müller committed
1
2
3
4
5
package de.tum.workflows

import foltl.FOLTL._
import blocks.WorkFlow._
import Implicits._
Christian Müller's avatar
Christian Müller committed
6
7
import com.typesafe.scalalogging.LazyLogging
import de.tum.workflows.ltl.LTL
Christian Müller's avatar
Christian Müller committed
8

Christian Müller's avatar
Christian Müller committed
9
object Main extends App with LazyLogging {
Christian Müller's avatar
Christian Müller committed
10

Christian Müller's avatar
Christian Müller committed
11
12
13
14
15
16
17
18
19
  val w = Workflow(
      Signature(Map(
          // first one is oracle
          ("O" -> List("s")),
          ("Q" -> List("x","s")),
          ("R" -> List("y","s")),
          ("S" -> List("x","y","s"))
      )),
      List(
Christian Müller's avatar
Christian Müller committed
20
21
22
23
      ForallMayBlock(List("x","s"),
          Add(Fun("O","s"),"Q", List("x","s"))
      ),
      Loop(List(
Christian Müller's avatar
Christian Müller committed
24
          ForallMayBlock(List("x","y","s"),
Christian Müller's avatar
Christian Müller committed
25
26
27
28
29
30
31
              Add(Fun("R", List("y","s")), "S", List("x","y","s"))
          ),
          ForallBlock(List("x","s"),
              Add(Fun("Q",List("x","s")), "R", List("x","s"))
          )
      ))
  ))
Christian Müller's avatar
Christian Müller committed
32
33
  
  logger.info(s"Workflow:\n$w")
Christian Müller's avatar
Christian Müller committed
34
35
  
  val res = Encoding.toFOLTL(w)
Christian Müller's avatar
Christian Müller committed
36
37
38
39
40
  
  // agent list
  val res2 = LTL.eliminateUniversals(res, List("a"))
  val res3 = LTL.eliminatePredicates(res2)
  logger.info(res3.toString())
Christian Müller's avatar
Christian Müller committed
41
}