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

allow omitting specs:

parent 1e60f6ad
Workflow
forallmay x:A,p:P
True → Conf += (x,p)
forallmay x:A,p:P
!Conf(x,p) → Assign += (x,p)
forall x:A,p:P,r:R
(Assign(x,p) ∧ O(x,p,r)) → Review += (x,p,r)
loop {
forall xa:A,xb:A,p:P,r:R (Assign(xa,p) ∧ Review(xb,p,r)) → Read += (xa,p,r)
forallmay x:A,p:P,r:R (Assign(x,p) ∧ O(x,p,r)) → Review += (x,p,r)
}
Declassify
O(x:A,p:P,r:R): G ¬ Conf(at:A,p:P)
Target
Read(at:A, bt:A, pt:P, rt:R)
Causality
a:A
# /bin/bash
TIMEOUT=20m
for RUN in 1 2 3 4 5 6 7 8 9 10
for RUN in 1
do
for FILE in results/*.ltl
do
......@@ -26,4 +26,4 @@ do
echo "Timeout after ${TIMEOUT}" >> ${METRICS}
fi
done
done
\ No newline at end of file
done
# /bin/bash
TIMEOUT=10s
TIMEOUT=20s
for FILE in results/*.ltl
do
......
results/conference-acceptance_causal.foltl: 727
results/conference-acceptance_causal.ltl: 5275
Universe: a:A, causalaA1:A, causalaP1:P, at:A, bt:A, pt:P
Measuring on Fri May 19 15:28:36 WEST 2017:
Timeout after 20s
Measuring run 1:
Timeout after 20m
results/conference-acceptance_stubborn.foltl: 628
results/conference-acceptance_stubborn.ltl: 1089
Universe: at:A, bt:A, pt:P
Measuring on Fri May 19 15:28:56 WEST 2017:
unsat
real 2.48
user 2.48
sys 0.00
Finished successfully
Measuring run 1:
unsat
real 2.49
user 2.48
sys 0.01
Finished successfully
results/conference_causal.foltl: 730
results/conference_causal.ltl: 8885
Universe: a:A, causalaA1:A, causalaP1:P, causalaR1:R, at:A, bt:A, pt:P, rt:R
Measuring on Fri May 19 15:28:59 WEST 2017:
Timeout after 20s
Measuring run 1:
Timeout after 20m
results/conference_linear_causal.foltl: 571
results/conference_linear_causal.ltl: 4278
Universe: a:X, causalaX1:X, causalaP1:P, causalaR1:R, xt:X, yt:X, pt:P
Measuring on Fri May 19 15:29:19 WEST 2017:
Timeout after 20s
Measuring run 1:
sat
real 103.16
user 103.07
sys 0.08
Finished successfully
results/conference_linear_stubborn.foltl: 469
results/conference_linear_stubborn.ltl: 698
Universe: xt:X, yt:X, pt:P
Measuring on Fri May 19 15:29:39 WEST 2017:
unsat
real 0.75
user 0.75
sys 0.00
Finished successfully
Measuring run 1:
unsat
real 0.79
user 0.78
sys 0.00
Finished successfully
results/conference_stubborn.foltl: 628
results/conference_stubborn.ltl: 1089
Universe: at:A, bt:A, pt:P, rt:R
Measuring on Fri May 19 15:29:39 WEST 2017:
unsat
real 2.47
user 2.46
sys 0.00
Finished successfully
Measuring run 1:
unsat
real 2.45
user 2.45
sys 0.00
Finished successfully
results/fixedarity10_stubborn.foltl: 1928
results/fixedarity10_stubborn.ltl: 5299
Universe: x:T, y:T
Measuring on Fri May 19 15:30:02 WEST 2017:
sat
real 0.85
user 0.80
sys 0.05
Finished successfully
Measuring run 1:
sat
real 0.85
user 0.80
sys 0.03
Finished successfully
results/fixedarity10safe_stubborn.foltl: 1924
results/fixedarity10safe_stubborn.ltl: 5283
Universe: x:T, y:T
Measuring on Fri May 19 15:29:42 WEST 2017:
Timeout after 20s
Measuring run 1:
unsat
real 33.35
user 33.32
sys 0.02
Finished successfully
results/fixedarity15_stubborn.foltl: 3963
results/fixedarity15_stubborn.ltl: 11114
Universe: x:T, y:T
Measuring on Fri May 19 15:30:23 WEST 2017:
sat
real 3.01
user 2.84
sys 0.16
Finished successfully
Measuring run 1:
sat
real 2.98
user 2.84
sys 0.14
Finished successfully
results/fixedarity15safe_stubborn.foltl: 3959
results/fixedarity15safe_stubborn.ltl: 11098
Universe: x:T, y:T
Measuring on Fri May 19 15:30:03 WEST 2017:
Timeout after 20s
Measuring run 1:
unsat
real 158.30
user 158.15
sys 0.11
Finished successfully
results/fixedarity20_stubborn.foltl: 6723
results/fixedarity20_stubborn.ltl: 19054
Universe: x:T, y:T
Measuring on Fri May 19 15:30:46 WEST 2017:
sat
real 16.55
user 16.22
sys 0.32
Finished successfully
Measuring run 1:
sat
real 16.28
user 15.98
sys 0.30
Finished successfully
results/fixedarity20safe_stubborn.foltl: 6719
results/fixedarity20safe_stubborn.ltl: 19038
Universe: x:T, y:T
Measuring on Fri May 19 15:30:26 WEST 2017:
Timeout after 20s
Measuring run 1:
unsat
real 745.79
user 745.47
sys 0.31
Finished successfully
results/incarity2_stubborn.foltl: 180
results/incarity2_stubborn.ltl: 335
Universe: x:T, y:T
Measuring on Fri May 19 15:31:02 WEST 2017:
unsat
real 0.10
user 0.10
sys 0.00
Finished successfully
Measuring run 1:
unsat
real 0.10
user 0.10
sys 0.00
Finished successfully
results/incarity3_stubborn.foltl: 301
results/incarity3_stubborn.ltl: 2206
Universe: x:T, y:T, z:T
Measuring on Fri May 19 15:31:02 WEST 2017:
unsat
real 6.17
user 6.14
sys 0.02
Finished successfully
Measuring run 1:
unsat
real 6.16
user 6.12
sys 0.03
Finished successfully
results/incarity4_stubborn.foltl: 451
results/incarity4_stubborn.ltl: 21894
Universe: u:T, v:T, w:T, x:T
Measuring on Fri May 19 15:31:09 WEST 2017:
Timeout after 20s
Measuring run 1:
Timeout after 20m
results/notebook_causal.foltl: 323
results/notebook_causal.ltl: 733
Universe: ac:User, causalacInfo1:Info, u:User, info:Info
Measuring on Fri May 19 15:31:29 WEST 2017:
unsat
real 1.03
user 1.03
sys 0.00
Finished successfully
Measuring run 1:
unsat
real 1.03
user 1.02
sys 0.00
Finished successfully
results/notebook_stubborn.foltl: 266
results/notebook_stubborn.ltl: 240
Universe: u:User, info:Info
Measuring on Fri May 19 15:31:30 WEST 2017:
unsat
real 0.15
user 0.15
sys 0.00
Finished successfully
Measuring run 1:
unsat
real 0.15
user 0.15
sys 0.00
Finished successfully
results/typedcausal2_causal.foltl: 364
results/typedcausal2_causal.ltl: 590
Universe: ca:T1, cb:T2, causalcbT11:T1, a1:T3, a2:T2
Measuring on Fri May 19 15:31:30 WEST 2017:
unsat
real 1.50
user 1.50
sys 0.00
Finished successfully
Measuring run 1:
unsat
real 1.47
user 1.46
sys 0.00
Finished successfully
results/typedcausal2_stubborn.foltl: 301
results/typedcausal2_stubborn.ltl: 202
Universe: a1:T3, a2:T2
Measuring on Fri May 19 15:31:31 WEST 2017:
unsat
real 0.01
user 0.01
sys 0.00
Finished successfully
Measuring run 1:
unsat
real 0.01
user 0.00
sys 0.00
Finished successfully
results/typedcausal3_causal.foltl: 539
results/typedcausal3_causal.ltl: 968
Universe: ca:T1, cb:T2, cc:T3, causalcbT11:T1, causalccT21:T2, a1:T4, a2:T3
Measuring on Fri May 19 15:31:31 WEST 2017:
sat
real 1.39
user 1.39
sys 0.00
Finished successfully
Measuring run 1:
sat
real 1.40
user 1.39
sys 0.00
Finished successfully
results/typedcausal3_stubborn.foltl: 447
results/typedcausal3_stubborn.ltl: 282
Universe: a1:T4, a2:T3
Measuring on Fri May 19 15:31:33 WEST 2017:
unsat
real 0.02
user 0.02
sys 0.00
Finished successfully
Measuring run 1:
unsat
real 0.01
user 0.01
sys 0.00
Finished successfully
results/typedcausal5_causal.foltl: 976
results/typedcausal5_causal.ltl: 2011
Universe: ca:T1, cb:T2, cc:T3, cd:T4, ce:T5, causalcbT11:T1, causalccT21:T2, causalcdT31:T3, causalceT41:T4, a1:T6, a2:T5
Measuring on Fri May 19 15:31:33 WEST 2017:
sat
real 17.27
user 17.24
sys 0.02
Finished successfully
Measuring run 1:
sat
real 17.05
user 17.02
sys 0.02
Finished successfully
results/typedcausal5_stubborn.foltl: 826
results/typedcausal5_stubborn.ltl: 481
Universe: a1:T6, a2:T5
Measuring on Fri May 19 15:31:50 WEST 2017:
unsat
real 0.02
user 0.02
sys 0.00
Finished successfully
Measuring run 1:
unsat
real 0.04
user 0.03
sys 0.00
Finished successfully
results/typedincarity10_stubborn.foltl: 1960
results/typedincarity10_stubborn.ltl: 1719
Universe: x:D, z:F, ac:I, v:B, ad:J, u:A, aa:G, ab:H, w:C, y:E
Measuring on Fri May 19 15:31:50 WEST 2017:
unsat
real 9.00
user 8.99
sys 0.00
Finished successfully
Measuring run 1:
unsat
real 8.97
user 8.96
sys 0.00
Finished successfully
results/typedincarity2_stubborn.foltl: 180
results/typedincarity2_stubborn.ltl: 163
Universe: x:A, y:B
Measuring on Fri May 19 15:31:59 WEST 2017:
unsat
real 0.02
user 0.02
sys 0.00
Finished successfully
Measuring run 1:
unsat
real 0.04
user 0.04
sys 0.00
Finished successfully
results/typedincarity3_stubborn.foltl: 301
results/typedincarity3_stubborn.ltl: 270
Universe: x:A, y:B, z:C
Measuring on Fri May 19 15:31:59 WEST 2017:
unsat
real 0.09
user 0.08
sys 0.00
Finished successfully
Measuring run 1:
unsat
real 0.10
user 0.10
sys 0.00
Finished successfully
results/typedincarity4_stubborn.foltl: 451
results/typedincarity4_stubborn.ltl: 402
Universe: u:A, v:B, w:C, x:D
Measuring on Fri May 19 15:31:59 WEST 2017:
unsat
real 0.19
user 0.18
sys 0.00
Finished successfully
Measuring run 1:
unsat
real 0.20
user 0.20
sys 0.00
Finished successfully
results/typedincarity5_stubborn.foltl: 630
results/typedincarity5_stubborn.ltl: 559
Universe: x:D, v:B, u:A, w:C, y:E
Measuring on Fri May 19 15:31:59 WEST 2017:
unsat
real 0.41
user 0.41
sys 0.00
Finished successfully
Measuring run 1:
unsat
real 0.40
user 0.40
sys 0.00
Finished successfully
results/university_causal.foltl: 389
results/university_causal.ltl: 871
Universe: cta:TA, cp:Prof, causalctaProf1:Prof, causalcpStudent1:Student, causalcpGrade1:Grade, as:Student, at:TA
Measuring on Fri May 19 15:32:00 WEST 2017:
sat
real 2.46
user 2.45
sys 0.00
Finished successfully
Measuring run 1:
sat
real 2.48
user 2.48
sys 0.00
Finished successfully
results/university_stubborn.foltl: 307
results/university_stubborn.ltl: 202
Universe: as:Student, at:TA
Measuring on Fri May 19 15:32:02 WEST 2017:
unsat
real 0.01
user 0.00
sys 0.00
Finished successfully
Measuring run 1:
unsat
real 0.02
user 0.01
sys 0.00
Finished successfully
......@@ -3,7 +3,7 @@ package de.tum.workflows
import scalax.collection.Graph // or scalax.collection.mutable.Graph
import scalax.collection.GraphPredef._
import scalax.collection.GraphEdge._
import scalax.collection.edge.LDiEdge // labeled directed edge
import scalax.collection.edge.LDiEdge // labeled directed edge
import scalax.collection.edge.Implicits._ // shortcuts
import blocks._
......@@ -16,47 +16,46 @@ import com.typesafe.scalalogging._
import scalax.collection.edge.LBase.LEdgeImplicits
object BlockImplicit extends LEdgeImplicits[SimpleBlock]; import BlockImplicit._
object Encoding extends LazyLogging {
type WorkflowGraph = Graph[Int, LDiEdge]
// Naming
// TODO: make sure there are no clashes
def nodeVar(n: Any) = Fun("n" + n, List())
def choiceVar(n: Any) = "choice" + n
def makeblock(b: Block, n1: Int, n2:Int, makeNode: (() => Int), makeId: (() => Block)):(List[LDiEdge[Int]]) = {
def makeblock(b: Block, n1: Int, n2: Int, makeNode: (() => Int), makeId: (() => Block)): (List[LDiEdge[Int]]) = {
b match {
// single edge
case b: SimpleBlock => {
List((n1 ~+> n2)(b))
}
case Loop(steps) => {
// add empty statement if loop ends with loop
val adjsteps = steps.last match {
case _:Loop => steps :+ makeId()
case _:Block => steps
case _: Loop => steps :+ makeId()
case _: Block => steps
}
// looping with n-1 nodes around n1
val newnodes = n1 +: (0 until adjsteps.size -1).toList.map(_ => makeNode()) :+ n1
val newnodes = n1 +: (0 until adjsteps.size - 1).toList.map(_ => makeNode()) :+ n1
// n1 -> n2, n2 -> n3, ...
val edgenodes = newnodes.sliding(2).toList
val edges = for ((step,List(start, end)) <- adjsteps.zip(edgenodes)) yield {
val edges = for ((step, List(start, end)) <- adjsteps.zip(edgenodes)) yield {
makeblock(step, start, end, makeNode, makeId)
}
edges.flatten :+ (n1 ~+> n2)(makeId())
}
case NondetChoice(l1, l2) => {
// make sure that at least one of the two branches has one node, so they will never build 2 edges between the same node
val newl1 = if (l1.length == l2.length && l1.length == 1) {
l1 :+ makeId()
} else l1
val newnodes1 = n1 +: (0 until newl1.size - 1).toList.map(_ => makeNode()) :+ n2
val edgenodes1 = newnodes1.sliding(2).toList
val edges1 = for ((step, List(start, end)) <- newl1.zip(edgenodes1)) yield {
......@@ -71,17 +70,17 @@ object Encoding extends LazyLogging {
}
}
}
def toGraph(w: Workflow):WorkflowGraph = {
def toGraph(w: Workflow): WorkflowGraph = {
var n1 = 0;
def newnode() = {
n1 = n1 + 1
n1
}
def makeid() = ForallBlock(List(), List())
val edges = (for ((step,i) <- w.steps.zipWithIndex) yield {
val edges = (for ((step, i) <- w.steps.zipWithIndex) yield {
if (i == w.steps.size - 1) {
val n = n1
val n2 = newnode()
......@@ -92,18 +91,18 @@ object Encoding extends LazyLogging {
}
}).flatten
var nodes = (0 until n1).toList
Graph.from(nodes, edges)
}
def encodeGraph(g: WorkflowGraph) = {
val allnodes = for (n <- g.nodes.toList) yield {
val list = n.outgoing.toList.map(e => nodeVar(e.to))
Implies(nodeVar(n), Next(Or.make(list:_*)))
val list = n.outgoing.toList.map(e => nodeVar(e.to))
Implies(nodeVar(n), Next(Or.make(list: _*)))
}
Globally(And.make(allnodes))
}
def encodeSanity(g: WorkflowGraph) = {
val negs = for (n <- g.nodes.toList; n2 <- g.nodes.toList if n < n2) yield {
Neg(And(nodeVar(n), nodeVar(n2)))
......@@ -113,77 +112,84 @@ object Encoding extends LazyLogging {
}
And.make(nodeVar(0), And.make(nodes), Globally(And.make(negs)))
}
def encodeStmt(s: Statement, pred: Option[Term]):(Term, String) = {
// var guard = s.guard
// for (p <- pred) { // if pred defined
// guard = And(guard, p)
// }
def encodeStmt(s: Statement, pred: Option[Term], bind: List[Var]): (Term, String) = {
// var guard = s.guard
// for (p <- pred) { // if pred defined
// guard = And(guard, p)