InvariantGenerator.scala 2.35 KB
Newer Older
Christian Müller's avatar
Christian Müller committed
1
package de.tum.niwo.invariants
Christian Müller's avatar
Christian Müller committed
2

3 4
import de.tum.niwo.blocks._
import de.tum.niwo.foltl.FOLTL._
Christian Müller's avatar
Christian Müller committed
5
import de.tum.niwo.foltl.Properties.{T1, T2}
Christian Müller's avatar
Christian Müller committed
6 7 8

object InvariantGenerator {
  
Christian Müller's avatar
Christian Müller committed
9 10
  def genEq(f: String, p: List[Var]) = {
    val newf = Fun(f, p)
Christian Müller's avatar
Christian Müller committed
11
    Equiv(newf.in(T1), newf.in(T2))
Christian Müller's avatar
Christian Müller committed
12
  }
Christian Müller's avatar
Christian Müller committed
13 14 15
  def genEq(f:Fun) = {
    Equiv(f.in(T1), f.in(T2))
  }
Christian Müller's avatar
Christian Müller committed
16

Christian Müller's avatar
Christian Müller committed
17 18 19 20 21 22 23 24 25 26 27 28 29
//  def invariantNoninterStubborn(spec: Spec) = {
//    val agent = spec.target.params(0)
//
//    val premise = And.make(for ((o, t) <- spec.declass) yield {
//      // Forall fv(o). (t_T1 or t_t2) -> G (o_T1 <-> o_T2)
//      Forall(o.freeVars().toList, Implies(Or(t.in(T1), t.in(T2)), Eq(o.in(T1), o.in(T2))))
//    })
//
//    val conclusion = And.make(for (r <- spec.w.sig.preds.toList if r.params.head.typ == agent.typ) yield {
//      val quant = r.params.drop(1)
//      Forall(quant, genEq(r, agent :: quant))
//    })
//
Christian Müller's avatar
Christian Müller committed
30
//    Forall(agent, premise → conclusion).simplify
Christian Müller's avatar
Christian Müller committed
31
//  }
Christian Müller's avatar
Christian Müller committed
32
  
Christian Müller's avatar
Christian Müller committed
33
  def invariantNoninterSingleBS(spec: NISpec) = {
Christian Müller's avatar
Christian Müller committed
34
    val agent = spec.target.params.head
Christian Müller's avatar
Christian Müller committed
35

Christian Müller's avatar
Christian Müller committed
36 37 38 39 40
//    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
Christian Müller's avatar
Christian Müller committed
41

Christian Müller's avatar
Christian Müller committed
42
    val conclusion = genEq(spec.target)
Christian Müller's avatar
Christian Müller committed
43
    Forall(spec.target.params, conclusion).simplify
Christian Müller's avatar
Christian Müller committed
44 45
    // Constants
//    conclusion
Christian Müller's avatar
Christian Müller committed
46 47
  }
  
Christian Müller's avatar
Christian Müller committed
48 49 50 51 52 53 54 55 56 57 58 59 60 61
//  def invariantNoninterStubbornBS(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 conclusion = And.make(for (r <- spec.w.sig.preds.toList if r.params.head.typ == agent.typ) yield {
//      val quant = r.params.drop(1)
//      Forall(quant, genEq(r, agent :: quant))
//    })
//
Christian Müller's avatar
Christian Müller committed
62
//    Forall(agent, Forall(quants, Implies(And.make(premise.map(_._2)), conclusion))).simplify
Christian Müller's avatar
Christian Müller committed
63
//  }
Christian Müller's avatar
Christian Müller committed
64

Christian Müller's avatar
Christian Müller committed
65
  def invariantAllEqual(spec: NISpec) = {
Christian Müller's avatar
Christian Müller committed
66 67
    And.make(for (r <- spec.w.sig.preds.toList if r.params.head.typ == spec.target.params.head.typ) yield {
      val params = r.params.map(v => Var(v.name + "t", v.typ))
Christian Müller's avatar
Christian Müller committed
68
      Forall(params, genEq(r.name, params))
Christian Müller's avatar
Christian Müller committed
69 70 71
    })
  }
}