add linear easychair, fix universal replacement

cnf.dimacs

-p cnf 35 44
-7 0
--7 8 0
--7 9 0
--8 -1 -2 0
--9 10 0
--9 11 0
--10 -1 -3 0
--11 12 0
--11 13 0
--12 -4 -1 0
--13 14 0
--13 15 0
--14 -4 -5 0
--15 16 0
--15 17 0
--16 -4 -2 0
--17 18 0
--17 19 0
--18 -4 -3 0
--19 20 0
--19 21 0
--20 -1 -5 0
--21 22 0
--21 23 0
--22 -2 -3 0
--23 24 0
--23 25 0
--24 -6 -5 0
--25 26 0
--25 27 0
--26 -6 -3 0
--27 28 0
--27 29 0
--28 -5 -3 0
--29 30 0
--29 31 0
--30 -6 -2 0
--31 32 0
--31 33 0
--32 -5 -2 0
--33 34 0
--33 35 0
--34 -6 -1 0
--35 -6 -4 0
+p cnf 24 29
+6 0
+-6 7 0
+-6 8 0
+-7 -1 -2 0
+-8 9 0
+-8 10 0
+-9 -1 -3 0
+-10 11 0
+-10 12 0
+-11 -1 -4 0
+-12 13 0
+-12 14 0
+-13 -1 -5 0
+-14 15 0
+-14 16 0
+-15 -2 -3 0
+-16 17 0
+-16 18 0
+-17 -2 -4 0
+-18 19 0
+-18 20 0
+-19 -2 -5 0
+-20 21 0
+-20 22 0
+-21 -3 -4 0
+-22 23 0
+-22 24 0
+-23 -3 -5 0
+-24 -4 -5 0

examples/easychair.spec

@@ -13,4 +13,4 @@ loop {
 
 Target
 
-(Conf(x,p) ∧ Read(xa, xb, p, r))
+(Conf(xa,p) ∧ Read(xa, xb, p, r))

examples/easychair_linear.spec

+Workflow
+
+forallmay x,p
+	True -> Conf += (x,p)
+forallmay x,p
+	!Conf(x,p) -> Ass += (x,p)
+forall x,p,r
+	(Ass(x,p) ∧ O(p,r)) -> Read += (x,p,r)
+forallmay y,x,p 
+	(Ass(x,p) ∧ Ass(y,p)) -> Comm += (x,y,p)
+
+Target
+
+(Conf(x,p) ∧ Comm(x, y, p))

src/main/scala/de/tum/workflows/ExampleWorkflows.scala

@@ -13,7 +13,7 @@ object ExampleWorkflows extends LazyLogging {
   val FOLDER = new File("examples")
   val ENDING = ".spec"
   
-  val examples = (for (f <- FOLDER.listFiles() if f.isFile() && f.getName.endsWith(".wf")) yield {
+  val examples = (for (f <- FOLDER.listFiles() if f.isFile() && f.getName.endsWith(ENDING)) yield {
     val s = Source.fromFile(f).mkString
     val spec = WorkflowParser.parseSpec(s)
     

src/main/scala/de/tum/workflows/Main.scala

@@ -14,6 +14,8 @@ import de.tum.workflows.blocks.Workflow
 
 object Main extends App with LazyLogging {
   
+  val MAXAGENTS = 5
+  
   def generateExample(name: String) {
       logger.info(s"Generating $name")
       val (wf, target) = ExampleWorkflows.examples(name)
@@ -31,6 +33,13 @@ object Main extends App with LazyLogging {
     val prop = Properties.noninterStubborn(w, target)
 
     val (agents, res) = LTL.eliminateExistentials(prop)
+    
+    logger.info(s"Using universe $agents")
+    if (agents.length > MAXAGENTS) {
+      logger.error(s"Universe of size ${agents.size} is too large. Aborting.")
+      return
+    }
+    
     val quantfree = LTL.eliminateUniversals(res, agents)
     val ltlprop = LTL.eliminatePredicates(quantfree)
 

src/main/scala/de/tum/workflows/Utils.scala

@@ -20,10 +20,4 @@ object Utils {
   def allchoices(w: Workflow) = {
     w.steps flatMap (collectChoices _) toSet
   }
-  
-  def allagents(t: Term) = {
-    t.collect({
-      case Fun(_, _, as) => as
-    })
-  }
 }
\ No newline at end of file

src/main/scala/de/tum/workflows/WorkflowParser.scala

@@ -82,4 +82,5 @@ object WorkflowParser extends RegexParsers {
   
   def parseWorkflow(s: String) = parseAll(WORKFLOW, s)
   def parseSpec(s: String) = parseAll(SPEC, s)
+  def parseTerm(s:String) = parseAll(TERM, s)
 }

src/main/scala/de/tum/workflows/foltl/FOLTL.scala

 package de.tum.workflows.foltl
 
 import de.tum.workflows.Utils
+import scala.annotation.tailrec
+
 //import de.tum.workflows.foltl.TermFunctions._
 
 object FOLTL {

src/main/scala/de/tum/workflows/foltl/Properties.scala

@@ -45,8 +45,8 @@ object Properties {
     val graph = toGraph(w)
     val cfg = sanecfg(graph)
     val sem = exec(w.sig, graph)
-    
-    val agents = allagents(target)
+
+    val agents = target freeVars() toList
     
     // choice and node predicates are equal in both runs (stubborn)
     val nodes = nodepredicates(graph) map (_.name)

src/main/scala/de/tum/workflows/ltl/LTL.scala

@@ -23,7 +23,6 @@ object LTL extends LazyLogging {
   
   def eliminateExistentials(t:Term) = {
     
-    // TODO: can't we improve this syntax?
     def coll:PartialFunction[Term, List[Var]] = {
       case Exists(a, term) => List.concat(a, term.collect(coll))
       // don't go over Foralls
@@ -31,7 +30,6 @@ object LTL extends LazyLogging {
       // don't go over Globally
       case Globally(_) => List.empty
     }
-    
     val agents = t.collect(coll)
     
     def elim:PartialFunction[Term, Term] = {
@@ -47,7 +45,7 @@ object LTL extends LazyLogging {
     (agents, res)
   }
   
-  // agents need to be distince names in t
+  // TODO: does not work for nested foralls
   def eliminateUniversals(t: Term, agents: List[Var]) = {
     
     if (agents.isEmpty) {
@@ -56,17 +54,14 @@ object LTL extends LazyLogging {
     
     t.everywhere({
         case Forall(tup, term) => {
-          
           val repl = comb(tup.size, agents)
           val terms = for (r <- repl) yield {
-            var newterm = term
-            for ((x,a) <- tup.zip(r)) {
-              newterm = newterm.everywhere({
-                // do replacement
-                case Fun(f, id, tup) => Fun(f, id, tup.map(v => if (x == v) a else v))
-              })
-            }
-            newterm
+            val mapping = tup.zip(r) toMap
+
+            term.everywhere({
+              // do replacement
+              case Fun(f, id, tup) => Fun(f, id, tup.map(a => mapping.getOrElse(a, a)))
+            })
           }
           And.make(terms)
         }

src/test/scala/de/tum/workflows/ltl/tests/LTLTests.scala

@@ -7,6 +7,7 @@ import org.scalatest.Inspectors._
 import de.tum.workflows.foltl.FOLTL._
 import de.tum.workflows.ltl.LTL
 import de.tum.workflows.Implicits._
+import de.tum.workflows.WorkflowParser
 
 class LTLSpec extends FlatSpec {
 
@@ -21,6 +22,12 @@ class LTLSpec extends FlatSpec {
 
     val f2 = Exists("x", Forall(List("y"), Fun("f", List("x", "y"))))
     LTL.eliminateUniversals(f2, List("a")) should be(Exists("x", Fun("f", List("x", "a"))))
+    
+    val f3 = Forall(List("x","y"), Fun("f", List("x", "y")))
+    val r = """
+        (f(x,x) ∧ f(y,x) ∧ f(x,y) ∧ f(y,y))   
+        """
+    LTL.eliminateUniversals(f3, List("x", "y")) should be(WorkflowParser.parseTerm(r).get)
   }
 
   "Existential elimination" should "work" in {
@@ -36,7 +43,7 @@ class LTLSpec extends FlatSpec {
     f.toString should be (
       "True ∧ False ∧ True ∧ False ∧ G False"
     )
-    
   }
   
+  
 }
\ No newline at end of file

src/test/scala/de/tum/workflows/ltl/tests/ParserTest.scala

@@ -10,7 +10,7 @@ import de.tum.workflows.Implicits._
 import de.tum.workflows.foltl.FOLTL._
 import com.typesafe.scalalogging.LazyLogging
 
-class ParserTest extends FlatSpec with LazyLogging {
+class ParserTest extends FlatSpec {
 
   def testResult(s: String, sig: Signature) {
     testResult(s, Workflow(sig, List()))
@@ -20,7 +20,7 @@ class ParserTest extends FlatSpec with LazyLogging {
     val parsed = WorkflowParser.parseWorkflow(s)
 
     if (!parsed.successful) {
-      logger.error(s"Parsing unsuccessful: $parsed")
+      info(s"Parsing unsuccessful: $parsed")
     }
 
     parsed.successful should be(true)
@@ -36,7 +36,7 @@ class ParserTest extends FlatSpec with LazyLogging {
     val parsed = WorkflowParser.parseSpec(s)
 
     if (!parsed.successful) {
-      logger.error(s"Parsing unsuccessful: $parsed")
+      info(s"Parsing unsuccessful: $parsed")
     }
 
     parsed.successful should be(true)