Commit c5981f8b authored by Christian Müller's avatar Christian Müller

add more functionality

parent 71ff4192
Workflow
forallmay x,s
True -> R += (x,s)
forallmay x,s
R(x,s) -> S += (x)
Target
S(x)
Workflow
// Why does it break if this is may?
forallmay x,s
True -> R += (x,s)
forall x,s
R(x,s) -> S += (x)
Target
S(x)
......@@ -2,6 +2,11 @@
shopt -s nullglob
TIMEOUT=1m
for FILE in results/*/*.png
do
rm $FILE
done
for FILE in results/*/*.dot
do
NAME=$(basename ${FILE} .dot)
......
......@@ -4,7 +4,7 @@ import foltl.FOLTL._
import blocks.Workflow._
import Implicits._
import com.typesafe.scalalogging.LazyLogging
import de.tum.workflows.ltl.LTL
import de.tum.workflows.ltl.FOTransformers
import de.tum.workflows.Utils._
import de.tum.workflows.foltl.Stubborn
import de.tum.workflows.foltl.Properties
......
......@@ -4,7 +4,7 @@ import foltl.FOLTL._
import blocks.Workflow._
import Implicits._
import com.typesafe.scalalogging.LazyLogging
import de.tum.workflows.ltl.LTL
import de.tum.workflows.ltl.FOTransformers
import de.tum.workflows.Utils._
import de.tum.workflows.foltl.Stubborn
import de.tum.workflows.foltl.Properties
......@@ -36,7 +36,7 @@ object MainLTL extends App with LazyLogging {
logger.info("Omitting spec - no embedding in LTL possible")
} else {
logger.info("Nonomitting spec - embedding FOLTL formula in LTL")
val (agents, res) = LTL.eliminateExistentials(prop)
val (agents, res) = FOTransformers.eliminateExistentials(prop)
val universe = agents.map(_.withType()).mkString(", ")
logger.info(s"Using universe $universe")
......@@ -46,8 +46,8 @@ object MainLTL extends App with LazyLogging {
return
}
val quantfree = LTL.eliminateUniversals(res, agents)
val ltlprop = LTL.eliminatePredicates(quantfree)
val quantfree = FOTransformers.eliminateUniversals(res, agents)
val ltlprop = FOTransformers.eliminatePredicates(quantfree)
metrics :+= s"${name}.ltl: ${ltlprop.opsize()}"
metrics :+= s"Universe: $universe"
......
......@@ -7,9 +7,10 @@ import de.tum.workflows.foltl.FOLTL
import de.tum.workflows.foltl.FOLTL._
import de.tum.workflows.foltl.FormulaFunctions._
import de.tum.workflows.foltl.FormulaFunctions
import de.tum.workflows.ltl.FOTransformers
object Preconditions extends LazyLogging {
def weakestPrecondition(f: Formula, b: SimpleBlock) = {
// TODO: f can't be temporal yet
val choice = b.pred.map(n => Fun(n, b.agents))
......@@ -33,7 +34,7 @@ object Preconditions extends LazyLogging {
}) toMap
// Replace literals with their precondition
f everywhere {
val replaced = f everywhere {
case Fun(name, ind, params) if b.steps.exists(s => s.fun == name) => {
val up = updates(name)
val renamed = up._2.parallelRename(up._1, params)
......@@ -46,6 +47,29 @@ object Preconditions extends LazyLogging {
}
}
}
replaced
}
def abstractPrecondition(f:Formula, b:SimpleBlock, stubborn:Boolean) = {
val precond = weakestPrecondition(f, b)
// Stubborn agents -> remove trace variable from choice predicate
val stubprecond = if (stubborn) {
precond.everywhere {
case Fun(f, i, p) if b.may && f == b.pred.get => Fun(f, p)
}
} else precond
// Abstract away inner existentials
val universalinv = FOTransformers.abstractExistentials(stubprecond).simplify()
// Abstract away auxilliaries
val auxless = if (b.pred.isDefined) {
FOTransformers.eliminateAuxiliaryPredicate(universalinv, b.pred.get).simplify()
} else {
universalinv
}
auxless
}
// TODO: Replace oracles and choices by fresh predicates?
......
......@@ -52,6 +52,9 @@ object Utils {
def write(name: String, prop: String) {
val file = new File(s"$RESULTSFOLDER/$name")
if (file.exists()) {
file.delete()
}
file.getParentFile.mkdirs()
val writer = new PrintWriter(file)
writer.print(prop)
......
......@@ -277,45 +277,62 @@ object FormulaFunctions extends LazyLogging {
}
}
def collectQuantifiersSub(f: Formula): List[(Boolean, Formula => Quantifier)] = {
def collectQuantifiers(f: Formula): List[(Boolean, List[Var])] = {
f collect {
case Exists(xs, fsub) => List((true, (t: Formula) => (Exists(xs, t)))) ++ collectQuantifiersSub(fsub)
case Forall(xs, fsub) => List((false, (t: Formula) => (Forall(xs, t)))) ++ collectQuantifiersSub(fsub)
case Exists(xs, fsub) => (true, xs) :: collectQuantifiers(fsub)
case Forall(xs, fsub) => (false, xs) :: collectQuantifiers(fsub)
case BinOp(make, f1, f2) => {
val q1 = collectQuantifiersSub(f1)
val q2 = collectQuantifiersSub(f2)
val q1 = collectQuantifiers(f1)
val q2 = collectQuantifiers(f2)
// Merge while trying to stay in BS, if possible
// TODO: could be improved to minimize quantifier alternations)
// TODO: merge universals with same type by renaming
val ex1 = q1.takeWhile(_._1)
val rest1 = q1.drop(ex1.size)
val ex2 = q2.takeWhile(_._1)
val rest2 = q2.drop(ex2.size)
// filter out same bound variables (TODO: could be improved if different names)
val existbound = ex1.flatMap(_._2)
val univbound = rest1.flatMap(_._2)
val exset = existbound.toSet
val univset = univbound.toSet
val ex2 = q2.takeWhile(_._1).map(q =>
(q._1, q._2.filterNot(exset.contains _))
)
val rest2 = q2.drop(ex1.size).map(q =>
(q._1, q._2.filterNot(univset.contains _))
)
ex1 ++ ex2 ++ rest1 ++ rest2
}
}
}
def collectQuantifiers(f: Formula) = {
collectQuantifiersSub(f).map(_._2)
def checkBindings(f:Formula) = {
def checkBindingsSub(f: Formula, bound:Set[Var]):List[Var] = {
f collect {
case Quantifier(make, xs, inner) => {
val conflicts = xs.filter(bound.contains _)
conflicts ++ checkBindingsSub(inner, bound ++ xs)
}
}
}
checkBindingsSub(f, Set()).isEmpty
}
def isBS(f: Formula) = {
val quantprefix = collectQuantifiersSub(f.toNegNf())
val quantprefix = collectQuantifiers(f.toNegNf())
// has no forall exists in quantifier prefix
!quantprefix.sliding(2).exists(list => !list(0)._1 && list(1)._1)
}
def toNegNf(f: Formula) = {
val bound = if (hasDuplicateBindings(f)) {
// logger.info(s"Formula binds variables more than once - renaming bindings: ${f.pretty}")
FormulaFunctions.fixBinding(f, Set())._1
} else f
val noeq = eliminateEq(bound)
// val bound = if (hasDuplicateBindings(f)) {
// // logger.info(s"Formula binds variables more than once - renaming bindings: ${f.pretty}")
// FormulaFunctions.fixBinding(f, Set())._1
// } else f
val noeq = eliminateEq(f)
eliminateImplication(noeq).simplify()
}
......@@ -360,15 +377,18 @@ object FormulaFunctions extends LazyLogging {
}
}
def toPrenex(f: Formula) = {
// TODO: make sure no quantifiers in scope of others with same name
def toPrenex(f: Formula):Formula = {
val negnf = f.toNegNf()
val (simp, boundVars) = fixBinding(negnf, Set())
// val (simp, boundVars) = fixBinding(negnf, Set())
// Simplify first to push negation inward
val quants = collectQuantifiers(simp)
val stripped = stripQuantifiers(simp)
val quants = collectQuantifiers(negnf)
val stripped = stripQuantifiers(negnf)
quants.foldRight(stripped)((quant, inner) => quant(inner))
quants.foldRight(stripped)((quant, inner) => {
if (quant._1) Exists(quant._2, inner) else Forall(quant._2, inner)
})
}
def toCNF(f: Formula) = {
......
......@@ -7,7 +7,7 @@ import de.tum.workflows.foltl.FOLTL._
import de.tum.workflows.foltl.FOLTL
import de.tum.workflows.foltl.FormulaFunctions
object LTL extends LazyLogging {
object FOTransformers extends LazyLogging {
// Computes all possible tuples of size i
def comb[T](types:List[String], universe:Map[String, List[T]]):List[List[T]] = {
......@@ -26,6 +26,50 @@ object LTL extends LazyLogging {
}
}
def collectClauses(f:Formula):List[List[Formula]] = {
def collectClause(f:Formula):List[Formula] = f collect {
case t:Var => List(t)
case t:Neg => List(t)
case t:Fun => List(t)
case Or(f1, f2) => collectClause(f1) ++ collectClause(f2)
}
def collectMultiClause(f:Formula):List[List[Formula]] = f collect {
case t:Or => List(collectClause(t))
case And(t1, t2) => collectMultiClause(t1) ++ collectMultiClause(t2)
}
collectMultiClause(f)
}
def eliminateAuxiliaryPredicate(f:Formula, AUX:String) = {
val cnf = f.toCNF()
val quantifiers = FormulaFunctions.collectQuantifiers(cnf)
// Inspect clauses
val clauses = FOTransformers.collectClauses(cnf)
val simped =
for (c <- clauses;
removeclause = (for (c1 <- c if (c.contains(Neg(c1)))) yield true)
if (removeclause.isEmpty)
) yield {
c
}
val form = And.make(simped.map(Or.make _))
// TODO: improve
val newform = quantifiers.foldRight(form)((q, inner) => if(q._1) Exists(q._2, inner) else Forall(q._2, inner))
// TODO: add equalities?
val repld = newform everywhere {
case Neg(Fun(AUX, _, _)) => False
case Fun(AUX, _, _) => False
}
repld.simplify()
}
/**
* Gobble up all outermost existential quantifiers
* Needs to have non-conflicting bindings
......@@ -119,16 +163,16 @@ object LTL extends LazyLogging {
}
val nf = f.toNegNf()
val (agents, inner) = LTL.eliminateExistentials(nf)
val (agents, inner) = FOTransformers.eliminateExistentials(nf)
val existbound = Exists(agents, inner)
LTL.eliminateUniversals(existbound, agents)
FOTransformers.eliminateUniversals(existbound, agents)
}
/**
* Instantiates existentials in AE formulae.
* Resulting formula is in NegNF
*/
def instantiateExistentials(f:Formula) = {
def abstractExistentials(f:Formula) = {
val neg = Neg(f).toNegNf().simplify()
// Check fragment
......@@ -139,7 +183,7 @@ object LTL extends LazyLogging {
// val (agents, inner) = LTL.eliminateExistentials(nf)
// val existbound = Exists(agents, inner)
val res = LTL.eliminateUniversals(neg, List())
val res = FOTransformers.eliminateUniversals(neg, List())
Neg(res).simplify()
}
}
\ No newline at end of file
......@@ -15,7 +15,7 @@ import de.tum.workflows.Preconditions
import de.tum.workflows.blocks._
import de.tum.workflows.foltl.FOLTL._
import de.tum.workflows.foltl.FormulaFunctions
import de.tum.workflows.ltl.LTL
import de.tum.workflows.ltl.FOTransformers
object InvariantChecker extends LazyLogging {
......@@ -41,7 +41,7 @@ object InvariantChecker extends LazyLogging {
val stripped = FormulaFunctions.stripQuantifiers(neg)
// val prefix = FormulaFunctions.collectQuantifiersSub(univfree)
val satform = LTL.eliminatePredicates(stripped)
val satform = FOTransformers.eliminatePredicates(stripped)
// Checking QFree
s.add(Z3QFree.translate(satform, ctx))
......@@ -59,19 +59,12 @@ object InvariantChecker extends LazyLogging {
}
def checkBlockInvariant(sig: Signature, b: SimpleBlock, pre: Formula, post: Formula, stubborn: Boolean, isfirst: Boolean) = {
val precond = Preconditions.weakestPrecondition(post, b)
// Stubborn agents -> remove trace variable from choice predicate
val stubprecond = if (stubborn) {
precond.everywhere {
case Fun(f, i, p) if b.may && f == b.pred.get => Fun(f, p)
}
} else precond
val precond = Preconditions.abstractPrecondition(post, b, stubborn)
// TODO: do we do this here?
val firstprecond = if (isfirst) {
stubprecond.assumeEmpty(sig.preds.map(_.name).toList)
} else { stubprecond }
precond.assumeEmpty(sig.preds.map(_.name).toList)
} else { precond }
// val test1 = inv.toPrenex()
// val test2 = stubprecond.toPrenex()
......@@ -118,23 +111,23 @@ object InvariantChecker extends LazyLogging {
// check if relabelled invariant still satisfiable
// never relabel initial node
if (!isfirst) {
val newinv = And(labels(next._1), Preconditions.weakestPrecondition(post, next)).simplify()
val newinv = And(labels(next._1), Preconditions.abstractPrecondition(post, next, stubborn)).simplify()
// Abstract away inner existentials
val universalinv = LTL.instantiateExistentials(newinv).simplify()
val (status2, solver2) = checkOnZ3(Implies(newinv, False))
// TODO: Abstract away auxilliaries
val (status2, solver2) = checkOnZ3(Implies(universalinv, False))
val nostrangebindings = FormulaFunctions.checkBindings(newinv)
if (!nostrangebindings) {
logger.error("New invariant binds variables more than once")
logger.error(s"Invariant would be $newinv")
}
// FIXME breaks if universalinv is used
val newlabels = labels.updated(next._1, newinv)
val invalidated = proven.filter(_._2 == next._1)
val newproven = (proven -- invalidated) + next
if (status2 == Status.SATISFIABLE) {
// Negation of newinv still sat, newinv does not imply false
// Negation of newinv still sat, newinv does not imply false)
logger.info(s"Relabeling ${next._1}. Continuing.")
checkInvariantRec(newlabels, newproven)
} else {
......
......@@ -2,7 +2,7 @@ package de.tum.workflows.toz3
import de.tum.workflows.blocks._
import de.tum.workflows.foltl.FOLTL._
import de.tum.workflows.ltl.LTL
import de.tum.workflows.ltl.FOTransformers
import de.tum.workflows.Implicits._
import de.tum.workflows.foltl.Properties.T1
......
......@@ -13,7 +13,7 @@ import de.tum.workflows.foltl.FOLTL._
import de.tum.workflows.Utils._
import de.tum.workflows.foltl.Properties
import Properties._
import de.tum.workflows.ltl.LTL
import de.tum.workflows.ltl.FOTransformers
import de.tum.workflows.ExampleWorkflows
import de.tum.workflows.blocks._
......@@ -111,7 +111,7 @@ class EncodingTest extends FlatSpec {
val s2 = Spec(w, List(), Fun("R", List("ax", "as")), List())
val prop = Properties.noninterStubborn(s2)
val (agents, res) = LTL.eliminateExistentials(prop)
val (agents, res) = FOTransformers.eliminateExistentials(prop)
agents should be (List(Var("ax"), Var("as")))
}
......
......@@ -32,6 +32,15 @@ class FOLTLTest extends FlatSpec {
And(t, t).simplify() should be (t)
}
it should "simplify double negation" in {
Neg(Neg(True)).simplify() should be(True)
}
it should "simplify quantors" in {
val f = And(Forall("x", Fun("f", "x")), Forall("x", Fun("f", "x")))
f.simplify() should be (Forall("x", Fun("f", "x")))
}
"Parallel rename" should "work on simple functions" in {
val f = And("a", Fun("f", List("b","a")))
......@@ -62,7 +71,9 @@ class FOLTLTest extends FlatSpec {
it should "rebind several things" in {
val f = And.make(Forall("x", "x"), Forall("x", "x"), Forall("x","x"))
println(f.toPrenex())
val p = f.toPrenex().simplify()
p should be (Forall(List("x","x1","x2"), And.make("x", "x1","x2")))
f.simplify().toPrenex() should be (Forall("x","x"))
}
it should "work on implication" in {
......@@ -91,9 +102,11 @@ class FOLTLTest extends FlatSpec {
it should "compute CNF for formulas with quantifiers" in {
val f = Or(And(Exists("c", "c"), "b"), And(Exists("c", "c"),"d"))
f.toCNF().simplify() should be (
Exists(List("c", "c1"), And(
And(Or("c", "c1"), Or("c","d")),
And(Or("b","c1"), Or("b","d"))
Exists(List("c", "c1"), And.make(
Or("c", "c1"),
Or("c","d"),
Or("b","c1"),
Or("b","d")
))
)
}
......
......@@ -5,30 +5,37 @@ import org.scalatest.Matchers._
import org.scalatest.Inspectors._
import de.tum.workflows.foltl.FOLTL._
import de.tum.workflows.ltl.LTL
import de.tum.workflows.ltl.FOTransformers
import de.tum.workflows.Implicits._
import de.tum.workflows.WorkflowParser
import de.tum.workflows.foltl.FormulaFunctions
class LTLSpec extends FlatSpec {
class FOTransformSpec extends FlatSpec {
"FOLTL simplification" should "simplify double negation" in {
Neg(Neg(True)).simplify() should be(True)
}
"universal elimination" should "work" in {
"Universal elimination" should "work" in {
val f = Globally(Forall(List("x", "y"), Fun("f", List("x", "y"))))
LTL.eliminateUniversals(f, List("a")) should be(Globally(Fun("f", List("a", "a"))))
FOTransformers.eliminateUniversals(f, List("a")) should be(Globally(Fun("f", List("a", "a"))))
val f2 = Exists("x", Forall(List("y"), Fun("f", List("x", "y"))))
LTL.eliminateUniversals(f2, List()) should be(Exists("x", Fun("f", List("x", "x"))))
FOTransformers.eliminateUniversals(f2, List()) should be(Exists("x", Fun("f", List("x", "x"))))
val f3 = Forall(List("x","y"), Fun("f", List("x", "y")))
val r = """
(f(x,x) ∧ f(x,y) ∧ f(y,x) ∧ f(y,y))
"""
LTL.eliminateUniversals(f3, List("x", "y")) should be(WorkflowParser.parseTerm(r).get)
FOTransformers.eliminateUniversals(f3, List("x", "y")) should be(WorkflowParser.parseTerm(r).get)
}
"Existential Abstraction" should "work" in {
val f = Forall("x", Exists("y", Fun("f", List("x", "y"))))
val univ = FOTransformers.abstractExistentials(f)
univ should be (Forall("x", Fun("f",List("x","x"))))
val f2 = Forall(List("x","y"), Exists("z", Fun("f", List("z", "z"))))
val univ2 = FOTransformers.abstractExistentials(f2)
univ2 should be (Forall(List("x","y"),
Or.make(Fun("f",List("x","x")), Fun("f", List("y","y")))))
}
it should "generate the correct types" in {
......@@ -37,23 +44,23 @@ class LTLSpec extends FlatSpec {
val p = Var("p","paper")
val f = Globally(Forall(List(x, p), Fun("f", List(x, p))))
LTL.eliminateUniversals(f, List(x, p)) should be (
FOTransformers.eliminateUniversals(f, List(x, p)) should be (
Globally(Fun("f", List(x,p)))
)
val x2 = Var("x2", "agent")
val f2 = Forall(List(x, p), Fun("f", List(x, p)))
val r2 = And(Fun("f", List(x,p)), Fun("f", List(x2, p)))
LTL.eliminateUniversals(f2, List(x, p, x2)) should be(r2)
FOTransformers.eliminateUniversals(f2, List(x, p, x2)) should be(r2)
val f3 = Forall(List(x, x2, p), Fun("f", List(x, x2, p)))
val r3 = And.make(Fun("f", List(x,x,p)), Fun("f", List(x, x2, p)), Fun("f", List(x2,x,p)), Fun("f", List(x2,x2,p)))
LTL.eliminateUniversals(f3, List(x, x2, p)) should be(r3)
FOTransformers.eliminateUniversals(f3, List(x, x2, p)) should be(r3)
}
"Existential elimination" should "work" in {
val test = Exists("a", And(Globally(Exists("b", True)), Exists("c", Forall("d", Exists("e", False)))))
LTL.eliminateExistentials(test) should be(
FOTransformers.eliminateExistentials(test) should be(
(List(Var("a"), Var("c")), And(Globally(Exists("b", True)), Forall("d", Exists("e", False)))))
}
......@@ -69,7 +76,7 @@ class LTLSpec extends FlatSpec {
"Existential Elimination" should "work in AE formulae" in {
val f = Forall(List("x","y"), Exists("z", Fun("f", List("x","z"))))
LTL.instantiateExistentials(f) should be (
FOTransformers.abstractExistentials(f) should be (
Forall(List("x","y"), Or(Fun("f", List("x","x")), Fun("f", List("x","y"))))
)
}
......@@ -121,4 +128,9 @@ class LTLSpec extends FlatSpec {
)
}
"getClauses" should "work" in {
val f = Exists("x", And(And(Or("f","g"), Or("a", Or("b","c"))), Or("d","e")))
val clauses:List[List[Var]] = List(List("f","g"), List("a", "b","c"), List("d","e"))
FOTransformers.collectClauses(f) should be (clauses)
}
}
\ No newline at end of file
......@@ -14,8 +14,10 @@ import de.tum.workflows.toz3.InvariantChecker
import de.tum.workflows.Encoding._
import de.tum.workflows.Utils
import de.tum.workflows.Encoding
import de.tum.workflows.ExampleWorkflows
import de.tum.workflows.toz3.InvariantChecker
class InvariantFilesTest extends FlatSpec {
class NonOmittingInvariantFilesTest extends FlatSpec {
"InvariantChecker" should "prove simple things safe" in {
val name = "tests/simpleNoChoice2"
......@@ -59,5 +61,4 @@ class InvariantFilesTest extends FlatSpec {
val o2 = Fun(name, Some("t2"), params)
Eq(o1, o2)
}
}
\ No newline at end of file
package de.tum.workflows.ltl.tests
import org.scalatest.FlatSpec
import org.scalatest.Matchers._
import org.scalatest.Inspectors._
import de.tum.workflows.foltl.FOLTL._
import de.tum.workflows.Implicits._
import de.tum.workflows.blocks._
import de.tum.workflows.Preconditions
import de.tum.workflows.foltl.FormulaFunctions
import de.tum.workflows.ExampleWorkflows
import de.tum.workflows.toz3.InvariantChecker
import de.tum.workflows.Encoding._
import de.tum.workflows.Utils
import de.tum.workflows.Encoding
class OmittingInvariantFilesTest extends FlatSpec {
// "InvariantChecker" should "prove simple things safe" in {
// val name = "tests/simpleOmittingNoChoice"
// val inv = Forall(List("x","s"), genEq("R",List("x","s")))
// assert(checkSafe(name, inv))
// }
it should "prove simple things safe" in {
val name = "tests/simpleOmittingNoChoice"
val inv = Forall(List("x"), genEq("S",List("x")))
assert(checkSafe(name, inv))
}
// "InvariantChecker" should "prove simple things safe" in {
// val name = "tests/simpleChoiceOmittingNoOracle"
// val inv =
// And(Forall(List("x"), genEq("S", List("x"))),
// Forall(List("x","s"), genEq("R",List("x","s")))
// )
// assert(checkSafe(name, inv))
// }
// it should "infer simple things safe" in {
// val name = "tests/simpleChoiceOmittingNoOracle"
// val inv = Forall(List("a"), genEq("S", List("a")))
// assert(checkSafe(name, inv))
// }
def checkSafe(name: String, inv: Formula) = {
val spec = ExampleWorkflows.parseExample(name).get
val (res, dot) = InvariantChecker.checkInvariantFP(spec.w, inv, true)
Utils.write(s"${name}.dot", dot)
res
}
def genEq(name: String, params: List[Var]) = {
val o1 = Fun(name, Some("t1"), params)
val o2 = Fun(name, Some("t2"), params)
Eq(o1, o2)
}
}
\ No newline at end of file
......@@ -7,7 +7,7 @@ import org.scalatest.Matchers._
import org.scalatest.Inspectors._
import de.tum.workflows.foltl.FOLTL._
import de.tum.workflows.ltl.LTL
import de.tum.workflows.ltl.FOTransformers
import de.tum.workflows.Implicits._
import de.tum.workflows.toz3._
import com.microsoft.z3.Context
......@@ -53,13 +53,13 @@ class Z3Test extends FlatSpec with LazyLogging with BeforeAndAfterEach {
val sprop = prop.simplify()
println(sprop.pretty())
val (agents, res) = LTL.eliminateExistentials(sprop)
val (agents, res) = FOTransformers.eliminateExistentials(sprop)
val universe = agents.map(_.withType()).mkString(", ")
logger.info(s"Using universe $universe")
val quantfree = LTL.eliminateUniversals(res, agents)
val ltlprop = LTL.eliminatePredicates(quantfree)
val quantfree = FOTransformers.eliminateUniversals(res, agents)
val ltlprop = FOTransformers.eliminatePredicates(quantfree)
val mapped = agents.groupBy(v => v.typ)
// maybe go to LTL and make all variables bool?
......
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