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

implication?

parent 369473be
...@@ -95,8 +95,8 @@ object InvariantChecker extends LazyLogging { ...@@ -95,8 +95,8 @@ object InvariantChecker extends LazyLogging {
val agent = spec.target.params(0) val agent = spec.target.params(0)
val premise = And.make(for ((o,t) <- spec.declass) yield { val premise = And.make(for ((o,t) <- spec.declass) yield {
// Forall fv(o). (t_T1 or t_t2) /\ G (o_T1 <-> o_T2) // Forall fv(o). (t_T1 or t_t2) -> G (o_T1 <-> o_T2)
Forall(o.freeVars().toList, And(Or(t.in(T1), t.in(T2)), Eq(o.in(T1), o.in(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 conclusion = And.make(for (r <- spec.w.sig.preds.toList if r.params.head.typ == agent.typ) yield {
......
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