Commit 64d2a9a9 authored by Christian Müller's avatar Christian Müller

add rendering

parent e259d7c8
......@@ -9,8 +9,8 @@ EclipseKeys.withBundledScalaContainers := false
libraryDependencies ++= Seq(
"com.typesafe.scala-logging" %% "scala-logging" % "3.5.0",
"ch.qos.logback" % "logback-classic" % "1.1.7",
"org.scalactic" %% "scalactic" % "3.0.1",
"org.scalatest" %% "scalatest" % "3.0.1" % "test",
"org.scalactic" %% "scalactic" % "3.0.4",
"org.scalatest" %% "scalatest" % "3.0.4" % "test",
"org.scala-graph" %% "graph-core" % "1.12.1",
"org.scala-graph" %% "graph-dot" % "1.12.1",
"org.scala-lang.modules" %% "scala-parser-combinators" % "1.0.5"
......
# /bin/bash
shopt -s nullglob
TIMEOUT=1m
for FILE in results/*/*.dot
do
NAME=$(basename ${FILE} .dot)
DIR=$(dirname "${FILE}")
PIC="${DIR}/${NAME}.png"
echo "Rendering ${FILE} to ${PIC}"
if
timeout ${TIMEOUT} time -p dot -Tpng < ${FILE} >> ${PIC}
then
echo "Finished successfully"
else
echo "Timeout after ${TIMEOUT}"
fi
done
......@@ -22,9 +22,10 @@ object MainInvariants extends App with LazyLogging {
logger.info(s"Encoding Spec:\n$spec")
def invariant =
InvariantGenerator.invariantNoninterStubbornBS _
// InvariantChecker.invariantNoninterStubborn _
// InvariantChecker.invariantAllEqual _
InvariantGenerator.invariantNoninterStubbornSingleBS _
// InvariantGenerator.invariantNoninterStubbornBS _
// InvariantChecker.invariantNoninterStubborn _
// InvariantChecker.invariantAllEqual _
val (t, (res, dot)) = time {
// InvariantChecker.checkInvariantOnce(spec.w, inv(spec), true)
......
......@@ -30,7 +30,22 @@ object InvariantGenerator {
Forall(agent, premise conclusion).simplify()
}
def invariantNoninterStubbornSingleBS(spec: Spec) = {
val agent = spec.target.params(0)
val premise = for ((o, t) <- spec.declass) yield {
// Forall fv(o). (t_T1 or t_t2) -> G (o_T1 <-> o_T2)
(o.freeVars().toList, Implies(Or(t.in(T1), t.in(T2)), Eq(o.in(T1), o.in(T2))))
}
val quants = premise.flatMap(_._1).toSet.toList // eliminate doubles
val quant = spec.target.params.drop(1)
val conclusion = Forall(quant, genEq(spec.target, agent :: quant))
Forall(agent, Forall(quants, Implies(And.make(premise.map(_._2)), conclusion))).simplify()
}
def invariantNoninterStubbornBS(spec: Spec) = {
val agent = spec.target.params(0)
......
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