Commit 25b85f4d authored by Christian Müller's avatar Christian Müller

better model parsing

parent eb3e8792
......@@ -69,10 +69,26 @@ object FOLTL {
object Fun {
def apply(name: String, params: List[Var]): Fun = Fun(name, None, params)
}
object FunFromVar {
val Predicate = "([a-zA-Z0-9]+)(#([a-zA-Z0-9]+))?((_[a-zA-Z0-9]+)*)".r
def unapply(s:String):Option[Fun] = {
s match {
case Predicate(name, null, _, tup, _*) => Some(Fun(name, None, tup split("_") drop(1) map (Var(_)) toList))
case Predicate(name, _, ind, tup, _*) => Some(Fun(name, Some(ind), tup split("_") drop(1) map (Var(_)) toList))
case _ => None
}
}
}
case class Fun(name: String, ind: Option[String], params: List[Var]) extends Formula {
override def toString() = name + Utils.mkString(ind, "(", "", ")") + params.map(_.name).mkString("(", ",", ")")
def updatedParams(index: Int, p:Var) = Fun(name, ind, params.updated(index, p))
def updatedParams(list: List[Var]) = Fun(name, ind, list)
def encodeToVar() = {
val pi = if (ind.isDefined) "#" + ind.get else ""
Var(name + pi + Utils.mkString(params, "_", "_", ""))
}
}
trait Quantifier extends Formula {
......
......@@ -96,14 +96,11 @@ object LTL extends LazyLogging {
}
/**
* Replace function calls Fun("f", List("x")) by Var("f_x")
* Replace function calls Fun("f", Some("t1"), List("x")) by Var("f#t1_x")
*/
def eliminatePredicates(t: Formula) = {
t.everywhere({
case Fun(f, ind, tup) => {
val pi = if (ind.isDefined) "_" + ind.get else ""
Var(f + pi + Utils.mkString(tup, "_", "_", ""))
}
case f:Fun => f.encodeToVar()
})
}
......
......@@ -37,7 +37,7 @@ object Z3 extends LazyLogging {
} else if (v.typ.equals("Bool")) {
ctx.getBoolSort()
} else {
ctx.mkFiniteDomainSort(v.typ, 1) // TODO: sort size?
ctx.mkFiniteDomainSort(v.typ, 3) // TODO: sort size?
}
v -> (Some(i), ctx.mkBound(i, sort), sort)
}) toMap
......@@ -270,8 +270,43 @@ object Z3 extends LazyLogging {
sb ++= "Evaluations:\n"
val sortedConsts = model.getConstDecls().sortBy(_.getName.toString())
for (f <- sortedConsts) {
val (l1, l2) = sortedConsts.partition(s => {
s.getName.toString() match {
case FunFromVar(_) => true
case _ => false
}
})
val funs = l1.map(s => {
val interp = model.getConstInterp(s)
(FunFromVar.unapply(s.getName.toString).get, interp.toString)
}) toList
val grouped = funs.groupBy(f => (f._1.name, f._1.ind))
// sort by name, path
val entries = grouped.iterator.toList.sortBy(_._1)
for (g <- entries) {
sb ++= g._1._1 + "(" + g._1._2 + "):\n"// name
// sort by value, variables
val tuples = g._2 sortBy(e => (e._2, e._1.params.mkString(",") ))
for ((fun, v) <- tuples) {
sb ++= fun.params.mkString("(",",",")") + " = " + v + "\n"
}
sb ++= "\n"
}
// Rest of the consts
for (f <- l2) {
val interp = model.getConstInterp(f)
val name = f.getName.toString match {
case FunFromVar(fun) => fun
case _ => f.getName.toString
}
sb ++= f.getName + " = " + interp.toString() + "\n"
}
......
......@@ -35,7 +35,7 @@ class ParserTest extends FlatSpec {
}
}
def testSpecResult(s: String, spec:blocks.Spec) {
def testSpecResult(s: String, spec: blocks.Spec) {
val parsed = WorkflowParser.parseSpec(s)
if (!parsed.successful) {
......@@ -144,17 +144,16 @@ class ParserTest extends FlatSpec {
forall x,y,s
O(s) -> R += (x,y,s)
"""
WorkflowParser.parseWorkflow(s).successful should be (false)
WorkflowParser.parseWorkflow(s).successful should be(false)
}
it should "parse typed variables" in {
val st = """
forallmay x:Agent,s:Paper
O(x) -> R += (x,s)
"""
val x = Var("x","Agent")
val s = Var("s","Paper")
val x = Var("x", "Agent")
val s = Var("s", "Paper")
val typedsig = Signature(Set(Fun("O", List(x))), Set(Fun("R", List(x, s))))
......@@ -162,7 +161,7 @@ class ParserTest extends FlatSpec {
typedsig,
List(
ForallMayBlock(List(x, s), "choice0",
Add(Fun("O", x), "R", List(x,s)))))
Add(Fun("O", x), "R", List(x, s)))))
testResult(st, w)
}
......@@ -216,4 +215,16 @@ class ParserTest extends FlatSpec {
testSpecResult(s, Spec(w, List((Fun("O", List("x")), True)), t, List()))
}
it should "parse encoded vars back to strings" in {
val s = "R1#t1_a_b"
val f = FunFromVar.unapply(s)
f should be(Some(Fun("R1", Some("t1"), List("a", "b"))))
val s2 = "R1_a_b"
val f2 = FunFromVar.unapply(s2)
f2 should be(Some(Fun("R1", None, List("a", "b"))))
}
}
\ No newline at end of file
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