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

update owl

parent e58d987c
(G(!p8|((((p0|p1)&Xp0)|(X!p0&!p0&!p1))&(((p6|p12)&Xp12)|(X!p12&!p6&!p12))&(((p2|p10)&Xp10)|(!p2&!p10&X!p10))&(((p5|p9)&Xp9)|(!p5&!p9&X!p9)))|X!p4)&!p0&!p3&!p4&!p7&!p9&!p10&!p11&!p12&!p13&p8&G(!p4|!p8)&F((!p9|!p13)&(p9|p13))&G(Xp4|!p8)&G(!p4|Xp4)&G(X!p4|(((Xp7&p7)|(X!p7&!p7))&((Xp3&p3)|(!p3&X!p3))&((X!p13&!p13)|(Xp13&p13))&((Xp11&p11)|(X!p11&!p11)))|!p4)&G(X!p4|(((p0&Xp0)|(!p0&X!p0))&((p10&Xp10)|(X!p10&!p10))&((p9&Xp9)|(X!p9&!p9))&((X!p12&!p12)|(Xp12&p12)))|!p4)&G(!p8|(((Xp7&(p1|p7))|(!p7&!p1&X!p7))&(((p6|p11)&Xp11)|(X!p11&!p6&!p11))&((Xp3&(p2|p3))|(X!p3&!p2&!p3))&(((p5|p13)&Xp13)|(!p5&!p13&X!p13)))|X!p4))
\ No newline at end of file
((F(!p13&p8)|F(p13&!p8))&!p2&!p1&!p0&G(!p5|!p2)&p5&G(!p2|(((X!p4&!p4)|(p4&Xp4))&((!p13&X!p13)|(p13&Xp13))&((Xp1&p1)|(X!p1&!p1))&((p11&Xp11)|(!p11&X!p11)))|X!p2)&G(!p2|(((Xp0&p0)|(X!p0&!p0))&((!p12&X!p12)|(p12&Xp12))&((Xp9&p9)|(X!p9&!p9))&((Xp8&p8)|(X!p8&!p8)))|X!p2)&G(X!p2|((((p13|p10)&Xp13)|(X!p13&!p13&!p10))&(((p11|p10)&Xp11)|(!p11&X!p11&!p10))&(((p7|p4)&Xp4)|(X!p4&!p7&!p4))&((!p1&X!p1&!p7)|((p7|p1)&Xp1)))|!p5)&G(X!p2|((((p8|p3)&Xp8)|(!p3&!p8&X!p8))&((Xp12&(p12|p3))|(!p3&X!p12&!p12))&((!p0&!p6&X!p0)|((p6|p0)&Xp0))&((!p9&X!p9&!p6)|(Xp9&(p9|p6))))|!p5)&!p13&!p12&!p11&G(!p5|Xp2)&!p9&!p8&G(Xp2|!p2)&!p4)
\ No newline at end of file
Manifest-Version: 1.0
Main-Class: de.tum.niwo.LTLCLI
......@@ -63,8 +63,9 @@ object MainInvariantsInference extends App with LazyLogging {
// clear()
// generateExample("nonomitting/conference")
generateExample("tests/conference_linear_small_withB", 1)
// generateExample("tests/conference_linear_small_withB", 1)
// generateExample("nonomitting/conference_linear", 2)
// generateExample("tests/loopexampleNoOracle")
// generateExample("tstests/easychair_singletrace")
// generateAllExamples()
}
......@@ -51,20 +51,24 @@ object MainLTL extends App with LazyLogging {
val owlform = OwlTransformer.toOwl(ltlprop)
val (t, sat) = time {
// simplify owl
val simped = SimplifierFactory.applyDefault(owlform.formula()).nnf()
write(name, s"$name.owlltl",simped.toString)
logger.info("Simplified owl formula")
// simplify owl
val (t1,simped) = time {
SimplifierFactory.apply(owlform.formula(), SimplifierFactory.Mode.SYNTACTIC_FIXPOINT)
}
write(name, s"$name.owlltl",simped.toString)
logger.info(s"Simplified owl formula in $t1 ms")
val (t2, sat) = time {
// check owl sat
logger.info("Checking satisfiability")
LanguageAnalysis.isSatisfiable(simped)
}
// LanguageAnalysis.isSatisfiable(simped)
logger.info(s"Found LTL formula to be satisfiable: $sat in $t ms")
OwlTransformer.isSatisfiable(simped)
}
logger.info(s"Found LTL formula to be satisfiable: $sat in $t2 ms")
metrics :+= s"Satisfiable: $sat"
metrics :+= s"Owl runtime: $t ms"
metrics :+= s"Owl simplification $t1 ms"
metrics :+= s"Owl runtime: $t2 ms"
write(name, s"$name.metrics", metrics.mkString("", "\n", "\n"))
}
......@@ -111,7 +115,7 @@ object MainLTL extends App with LazyLogging {
// clear()
// generateExample("nonomitting/conference")
// generateExample("tests/declasstest")
// generateExample("tests/simpleChoice")
generateExample("tests/simpleChoiceNoOracle")
generateExample("tests/simpleChoice")
// generateExample("tests/simpleChoiceNoOracle")
// generateAllExamples()
}
\ No newline at end of file
......@@ -35,7 +35,7 @@ object Utils extends LazyLogging {
}
def indentLines(s: String): String = {
s.lines.map(" " + _).mkString("\n")
s.linesIterator.map(" " + _).mkString("\n")
}
def time[R](block: => R): (Long, R) = {
......@@ -150,7 +150,7 @@ object Utils extends LazyLogging {
s"""Name: $name
|Description: $desc
| Invariant:
|${spec.inv.pretty.lines.map(s => " " + s).mkString("\n")}
|${spec.inv.pretty.linesIterator.map(s => " " + s).mkString("\n")}
| Model: $model
| Result: ${if (!res) "not " else ""}inductive
| WF size: $wfsize
......
......@@ -61,7 +61,7 @@ object FOLTL {
// indent
var opens = 0
val indented = for (line <- broken.lines) yield {
val indented = for (line <- broken.linesIterator) yield {
val indent = " " * (opens * 2)
val ret = indent + line
opens += line.count(_ == '(')
......
......@@ -212,7 +212,7 @@ object InvariantChecker extends LazyLogging {
msg ++= s"Possibly unsafe: Block may not uphold invariant:\n\n${e.label}\n\n"
if (res == Status.SATISFIABLE) {
msg ++= "Satisfying model:\n"
msg ++= Z3FOEncoding.printModel(solver.getModel()).lines.map(" " + _).mkString("\n")
msg ++= Z3FOEncoding.printModel(solver.getModel()).linesIterator.map(" " + _).mkString("\n")
} else if (res == Status.UNKNOWN) {
msg ++= s"Z3 result: $res (${solver.getReasonUnknown()})\n"
}
......
......@@ -2,11 +2,41 @@ package de.tum.niwo.owltransformer
import scala.collection.JavaConverters._
import com.typesafe.scalalogging.LazyLogging
import de.tum.niwo.Implicits.toList
import de.tum.niwo.foltl.FOLTL
import de.tum.niwo.foltl.FOLTL._
import owl.ltl._
import owl.automaton.acceptance.{GeneralizedBuchiAcceptance, GeneralizedRabinAcceptance, RabinAcceptance}
import owl.automaton.algorithms.LanguageEmptiness
import owl.grammar.LTLParser
import owl.ltl.parser.LtlParser
import owl.ltl.{Formula, _}
import owl.run.DefaultEnvironment
import owl.translations.ltl2dra.SymmetricDRAConstruction
import owl.translations.ltl2ldba.{AsymmetricLDBAConstruction, SymmetricLDBAConstruction}
object OwlTransformer extends LazyLogging {
// TODO: fix this as soon as Owl can do this better
def isSatisfiable(simped: Formula): Boolean = {
simped match {
case simped:Disjunction => simped.children.asScala.exists(isSatisfiable(_))
case simped:Conjunction => simped.children.asScala.forall(isSatisfiable(_))
case simped:Biconditional => isSatisfiable(simped.left) == isSatisfiable(simped.right)
case _ => {
val s = simped.toString
val p = LtlParser.parse(s)
logger.info(s"${p.variables()}: $p")
val construction = SymmetricLDBAConstruction.of(
DefaultEnvironment.of(false),
classOf[GeneralizedBuchiAcceptance]
)
val automaton = construction(p)
!LanguageEmptiness.isEmpty(automaton.copyAsMutable())
}
}
}
case class IndexedVariable(v:Var, index:Int) extends FOLTL.Formula
......@@ -76,7 +106,7 @@ object OwlTransformer extends LazyLogging {
case Equiv(f1, f2) => {
val e1 = transform(f1)
val e2 = transform(f2)
Biconditional.of(e1, e2).nnf()
Biconditional.of(e1, e2)
}
case Or(f1, f2) => {
......
......@@ -5,7 +5,6 @@ import java.util.HashMap
import com.microsoft.z3.Status
import de.tum.niwo.toz3.Z3LTL
import org.omg.CORBA.TIMEOUT
import de.tum.niwo.Implicits._
import com.microsoft.z3.Model
import de.tum.niwo.Examples
......
......@@ -9,13 +9,11 @@ import de.tum.niwo.owltransformer.OwlTransformer
import org.scalatest.FlatSpec
import org.scalatest.Matchers._
import org.scalatest.Inspectors._
import owl.automaton.algorithms.{EmptinessCheck, LanguageAnalysis}
import owl.automaton.algorithms.LanguageEmptiness
import owl.ltl.parser.LtlParser
import owl.run.{DefaultEnvironment, RunUtil}
import owl.translations.SimpleTranslations
import owl.translations.ltl2dra.LTL2DRAFunction
import owl.translations.ltl2ldba.LTL2LDBAFunction
import owl.translations.ltl2ldba.LTL2LDBAFunction.Configuration
import owl.translations.LTL2DAFunction
import owl.translations.LTL2DAFunction.Constructions._
class OwlTest extends FlatSpec with LazyLogging {
......@@ -50,9 +48,21 @@ class OwlTest extends FlatSpec with LazyLogging {
for (t <- tests) {
val owlform = OwlTransformer.toOwl(t._1)
val env = DefaultEnvironment.of(true, false, false)
val trans = SimpleTranslations.buildSafety(owlform, env)
val empty = EmptinessCheck.isEmpty(trans)
val env = DefaultEnvironment.of(false)
val set = EnumSet.of(
SAFETY,
CO_SAFETY,
BUCHI,
GENERALIZED_BUCHI,
CO_BUCHI,
PARITY,
RABIN,
GENERALIZED_RABIN
)
val ltl2da = new LTL2DAFunction(env, true, set)
val trans = ltl2da.apply(owlform)
val empty = LanguageEmptiness.isEmpty(trans)
empty should be (t._2)
}
......
......@@ -6,20 +6,19 @@ import org.scalatest.FlatSpec
class TSLeaderElectionTest extends FlatSpec {
def check(name:String, properties:InvProperties):Boolean = {
val spec = Examples.parseExampleTS(name).get
def check(name:String, properties:InvProperties):Boolean = {
val spec = Examples.parseExampleTS(name).get
Utils.check(name, "", spec, properties)
}
val properties = InvProperties(stubborn = true, eliminateA = true, eliminateB = true)
Utils.check(name, "", spec, properties)
}
"Deterministic Leader election" should "be proven safe" in {
val name = "tstests/leaderelection_inductive"
val properties = InvProperties(stubborn = true, eliminateA = true, eliminateB = true)
assert(check(name, properties))
}
"Deterministic Leader election" should "be proven safe" in {
val name = "tstests/leaderelection_inductive"
assert(check(name, properties))
}
it should "be proven safe with Bs" in {
val name = "tstests/leaderelection_inductive_withB"
......
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