InvariantGenerator.scala 2.45 KB
Newer Older
Christian Müller's avatar
Christian Müller committed
1 2 3 4
package de.tum.workflows.toz3

import de.tum.workflows.blocks._
import de.tum.workflows.foltl.FOLTL._
Christian Müller's avatar
Christian Müller committed
5
import de.tum.workflows.foltl.FOTransformers
Christian Müller's avatar
Christian Müller committed
6 7 8 9 10 11 12 13 14
import de.tum.workflows.Implicits._

import de.tum.workflows.foltl.Properties.T1
import de.tum.workflows.foltl.Properties.T2

object InvariantGenerator {
  
  def genEq(f: Fun, p: List[Var]) = {
    val newf = f.parallelRename(f.params, p)
Christian Müller's avatar
Christian Müller committed
15
    Equiv(newf.in(T1), newf.in(T2))
Christian Müller's avatar
Christian Müller committed
16 17
  }

Christian Müller's avatar
Christian Müller committed
18 19 20 21 22 23 24 25 26 27 28 29 30
//  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
31
//    Forall(agent, premise → conclusion).simplify
Christian Müller's avatar
Christian Müller committed
32
//  }
Christian Müller's avatar
Christian Müller committed
33
  
Christian Müller's avatar
Christian Müller committed
34
  def invariantNoninterSingleBS(spec: Spec) = {
Christian Müller's avatar
Christian Müller committed
35
    val agent = spec.target.params.head
Christian Müller's avatar
Christian Müller committed
36

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

Christian Müller's avatar
Christian Müller committed
43
    val conclusion = genEq(spec.target, spec.target.params)
Christian Müller's avatar
Christian Müller committed
44
    Forall(spec.target.params, conclusion).simplify
Christian Müller's avatar
Christian Müller committed
45 46
    // Constants
//    conclusion
Christian Müller's avatar
Christian Müller committed
47 48
  }
  
Christian Müller's avatar
Christian Müller committed
49 50 51 52 53 54 55 56 57 58 59 60 61 62
//  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
63
//    Forall(agent, Forall(quants, Implies(And.make(premise.map(_._2)), conclusion))).simplify
Christian Müller's avatar
Christian Müller committed
64
//  }
Christian Müller's avatar
Christian Müller committed
65 66

  def invariantAllEqual(spec: Spec) = {
Christian Müller's avatar
Christian Müller committed
67 68 69
    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))
      Forall(params, genEq(r, params))
Christian Müller's avatar
Christian Müller committed
70 71 72
    })
  }
}