InvariantCausalFilesTest.scala 4.75 KB
Newer Older
Christian Müller's avatar
Christian Müller committed
1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
26
27
28
29
30
31
32
33
34
35
36
37
38
39
40
41
42
43
44
45
46
47
48
49
50
51
52
53
54
55
56
57
58
59
60
61
62
63
64
65
66
67
68
69
70
71
72
73
74
75
76
77
78
79
80
81
82
83
84
85
86
87
88
89
90
91
92
93
94
95
96
97
98
99
100
101
102
103
104
105
106
107
108
109
110
111
112
113
114
115
116
117
118
119
120
121
122
123
124
125
126
127
128
129
130
131
132
133
134
135
package de.tum.workflows.ltl.tests.papertests

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

import de.tum.workflows.tests.TestUtils._
import de.tum.workflows.foltl.Properties
import de.tum.workflows.toz3.InvariantGenerator

class InvariantCausalFilesTest extends FlatSpec {
    
//  it should "fail to prove conference_linear" ignore {
//    val name = "nonomitting/conference_linear"
//    val xt = Var("xt","X")
//    val yt = Var("yt","X")
//    val pt = Var("pt","P")
//    val inv = Forall(List(xt, pt, yt), genEq("Comm", List(xt, yt, pt)))
//    assert(!checkSafeCausal(name, inv))
//  }
//  
//  it should "fail to prove conference_linear alleq" in {
//    val name = "nonomitting/conference_linear"
//    val inv = InvariantGenerator.invariantAllEqual(ExampleWorkflows.parseExample(name).get)
//    assert(!checkSafeCausal(name, "alleq", inv))
//  }
//  
//  // HEAP SPACE
//  it should "fail to prove conference_linear with elim" ignore {
//    val name = "nonomitting/conference_linear"
//    val xt = Var("xt","X")
//    val yt = Var("yt","X")
//    val pt = Var("pt","P")
//    val inv = Forall(List(xt, pt, yt), genEq("Comm", List(xt, yt, pt)))
//    assert(!checkSafeCausalElim(name, inv))
//  }
//  
//  // takes about 30s
//  it should "fail to prove nonomitting/conference" in {
//    val name = "nonomitting/conference"
//    val xt = Var("xat","X")
//    val yt = Var("xbt","X")
//    val pt = Var("pt","P")
//    val rt = Var("rt","R")
//    val inv = Forall(List(xt, yt, pt, rt), genEq("Read", List(xt, yt, pt, rt)))
//    assert(!checkSafeCausal(name, inv))
//  }
//  
//  // takes forever (up to 8s Z3 calls :(, simplification gets rid of 11mio chars), but passes
//  it should "fail to prove nonomitting/conference alleq" ignore {
//    val name = "nonomitting/conference"
//    val inv = InvariantGenerator.invariantAllEqual(ExampleWorkflows.parseExample(name).get)
//    assert(!checkSafeCausal(name, "alleq", inv))
//  }
//  
//  // HEAP SPACE
//  it should "fail to prove nonomitting/conference with elim" ignore {
//    val name = "nonomitting/conference"
//    val xt = Var("xat","X")
//    val yt = Var("xbt","X")
//    val pt = Var("pt","P")
//    val rt = Var("rt","R")
//    val inv = Forall(List(xt, pt, yt, rt), genEq("Read", List(xt, yt, pt, rt)))
//    assert(!checkSafeCausalElim(name, inv))
//  }
//  
//  // about 20 secs
//  it should "fail to prove omitting/conference" in {
//    val name = "omitting/conference"
//    val xt = Var("xat","X")
//    val pt = Var("pt","P")
//    val rt = Var("rt","R")
//    val inv = Forall(List(xt, pt), genEq("Read", List(xt, pt, rt)))
//    assert(!checkSafeCausal(name, inv))
//  }
//  
//  // about 60 seconds
//  it should "fail to prove omitting/conference alleq" in {
//    val name = "omitting/conference"
//    val inv = InvariantGenerator.invariantAllEqual(ExampleWorkflows.parseExample(name).get)
//    assert(!checkSafeCausal(name, "alleq", inv))
//  }
  
//  it should "prove omitting/conference_fixed" in {
//    val name = "omitting/conference_fixed"
//    val xt = Var("xt","A")
//    val pt = Var("rt","R")
//    val inv = Forall(List(xt, pt), genEq("Read", List(xt, pt)))
//    assert(checkSafeCausal(name, inv))
//  }
//  
//  it should "prove omitting/conference_fixed alleq" ignore {
//    val name = "omitting/conference_fixed"
//    val inv = InvariantGenerator.invariantAllEqual(ExampleWorkflows.parseExample(name).get)
//    assert(checkSafeCausal(name, "alleq", inv))
//  }
//  
//  it should "prove conference_linear_fixed" in {
//    val name = "omitting/conference_linear_fixed"
//    val xt = Var("xt","X")
//    val yt = Var("yt","X")
//    val pt = Var("pt","P")
//    val inv = Forall(List(xt, pt, yt), genEq("Comm", List(xt, yt, pt)))
//    assert(checkSafeCausal(name, inv))
//  }
//  
//  // maybe errors?
//  it should "prove conference_linear_fixed alleq" ignore {
//    val name = "omitting/conference_linear_fixed"
//    val inv = InvariantGenerator.invariantAllEqual(ExampleWorkflows.parseExample(name).get)
//    assert(checkSafeCausal(name, "alleq", inv))
//  }
//  
//  // HEAP SPACE
//  it should "fail to prove omitting/conference with elim" ignore {
//    val name = "omitting/conference"
//    val xt = Var("xat","X")
//    val pt = Var("pt","P")
//    val rt = Var("rt","R")
//    val inv = Forall(List(xt, pt), genEq("Read", List(xt, pt, rt)))
//    assert(!checkSafeCausalElim(name, inv))
//  }
    
}