[/] [trunk/] [src/] [maketest/] [clockexpression.sml] - Rev 35
(* $Id: clockexpression.sml 35 2008-04-01 02:55:38Z tbourke $ *)
structure ClockExpression :> CLOCK_EXPRESSION =
let structure E = Expression
and Env = Environment
and ECVT = ExpressionCvt
in struct
exception NonClockTerm
type symbol = Atom.atom
and symbolset = AtomSet.set
and var = Expression.var
datatype clockrel = Lt | Leq | Eq | Geq | Gt
datatype clockval = Simple of int
| Complex of E.expr
datatype clockterm = NonClock of E.expr
| CRel of E.var * clockrel * clockval
| CDiff of E.var * var * clockrel * clockval
datatype t = Term of clockterm
| And of t * t
| Or of t * t
val trueExpr = Term (NonClock E.trueExpr)
val falseExpr = Term (NonClock E.falseExpr)
(* shortcuts over Atom and AtomSet *)
infix <+ <- ++ <\ \ =:= ; open Symbol
local (*{{{1*)
(* TODO: fix smlnj-lib and replace with:
fun pad n = Iterate.iterate (fn s=> " " ^ s) n ""*)
fun pad n = let fun iter (s, 0) = s
| iter (s, n) = iter (s ^ " ", n - 1)
in iter ("", n) end
fun clkRelToStr Lt = " < " | clkRelToStr Leq = " <= "
| clkRelToStr Eq = " = " | clkRelToStr Geq = " >= "
| clkRelToStr Gt = " > "
fun clkValToStr (Simple i) = Int.toString i
| clkValToStr (Complex e) = "#" ^ ECVT.Expr.toString e ^ "#"
fun clkTermToStr (NonClock e) = "#" ^ ECVT.Expr.toString e ^ "#"
| clkTermToStr (CRel (s, rel, v)) = ECVT.Var.toString s ^
clkRelToStr rel ^
clkValToStr v
| clkTermToStr (CDiff (s1, s2, rel, v)) = ECVT.Var.toString s1 ^
" - " ^
ECVT.Var.toString s2 ^
clkRelToStr rel ^
clkValToStr v
in (*}}}1*)
fun clkToStr (n, Term t) = pad n ^ clkTermToStr t
| clkToStr (n, And (c1, c2)) = clkEToStr (n, "&&", c1, c2)
| clkToStr (n, Or (c1, c2)) = clkEToStr (n, "||", c1, c2)
and clkEToStr (n, s, c1, c2) = clkToStr (n + 1, c1)
^ "\n" ^ pad n ^ s ^ "\n"
^ clkToStr (n + 1, c2)
fun toString t = clkToStr (0, t)
end (* local *)
local (*{{{1*)
fun negRel Lt = Geq
| negRel Leq = Gt
| negRel Geq = Lt
| negRel Gt = Leq
| negRel Eq = raise Fail "ClockExpression.negRel: Cannot negate Eq"
fun negT (NonClock e) = Term (NonClock (E.negate e))
| negT (CRel (c, Eq, e)) = Or (Term (CRel (c, Lt, e)),
Term (CRel (c, Gt, e)))
| negT (CDiff (c1, c2, Eq, e)) = Or (Term (CDiff (c1, c2, Lt, e)),
Term (CDiff (c1, c2, Gt, e)))
| negT (CRel (c, rel, e)) = Term (CRel (c, negRel rel, e))
| negT (CDiff (c1, c2, rel, e)) = Term (CDiff (c1, c2, negRel rel, e))
in (*}}}1*)
fun negate (Term t) = negT t
| negate (And (e1, e2)) = Or (negate e1, negate e2)
| negate (Or (e1, e2)) = And (negate e1, negate e2)
end
fun getValFree (Simple _) = emptyset
| getValFree (Complex e) = E.getFreeNames e
val getVarFree = E.getFreeNames o E.VarExpr
fun getTermFree (NonClock e) = E.getFreeNames e
| getTermFree (CRel (s, _, cv)) = getVarFree s ++ getValFree cv
| getTermFree (CDiff (s1, s2, _, cv)) = getVarFree s1 ++ getVarFree s2
++ getValFree cv
fun getFree (And (c1, c2)) = getFree c1 ++ getFree c2
| getFree (Or (c1, c2)) = getFree c1 ++ getFree c2
| getFree (Term t) = getTermFree t
local (*{{{1*)
fun isClk (env, v) = case Env.findVarExprType env v
of SOME (E.CLOCK) => true
| NONE => raise NonClockTerm
| _ => false
fun isClkVar (env, E.VarExpr v) = isClk (env, v)
| isClkVar _ = false
fun containsClocks (env, expr) =
not (List.null (Env.filter (fn (env',e)=>isClkVar (env', e)) env expr))
fun notClk (env, e) = if containsClocks (env, e)
then raise NonClockTerm
else Term (NonClock e)
fun toRel E.LtOp = Lt | toRel E.LeOp = Leq
| toRel E.EqOp = Eq | toRel E.NeOp = raise NonClockTerm
| toRel E.GeOp = Geq | toRel E.GtOp = Gt
fun flipRel Lt = Gt | flipRel Leq = Geq
| flipRel Eq = Eq | flipRel Geq = Leq
| flipRel Gt = Lt
val toFlipRel = flipRel o toRel
fun toVal (E.IntCExpr i) = Simple i
| toVal e = Complex e
fun toVar (E.VarExpr v) = v
| toVar _ = raise Fail "toVar: bad call"
in (*}}}1*)
fun rename (r, clockexpr) = let
fun rCVar v = let val E.VarExpr v' = E.renameVar (r, E.VarExpr v)
in v' end
fun rCVal (s as Simple _) = s
| rCVal (Complex e) = Complex (E.renameVar (r, e))
fun rCTerm (NonClock e) = NonClock (E.renameVar (r, e))
| rCTerm (CRel (s, rel, cv)) = CRel (rCVar s, rel, rCVal cv)
| rCTerm (CDiff (s1, s2, rel, cv)) = CDiff (rCVar s1, rCVar s2,
rel, rCVal cv)
fun ren (Term t) = Term (rCTerm t)
| ren (And (c1, c2)) = And (ren c1, ren c2)
| ren (Or (c1, c2)) = Or (ren c1, ren c2)
in ren clockexpr end
local
fun addNameTypes xs = let
fun add ((n, _), s) = s <+ n
in foldl add emptyset xs end
in
fun ensureNoBindingConflict (rb, re) (b, e) = let
val rbn = addNameTypes rb
val bn = addNameTypes b
fun checkName ((n, ty), (bs, e, used)) =
if n <- rbn
then let val n' = getNewName (n, used)
in ((n', ty)::bs,
rename ({old=n, new=n'}, e),
used <+ n')
end
else ((n, ty)::bs, e, used)
val (b', e', _) = foldl checkName ([], e, rbn ++ bn) (rev b)
in (b', e') end
end (* local *)
(* raises NonClockTerm *)
fun fromExpr (usednames, env, expr) = let
val used = ref usednames
val forallbindings = ref ([] : (symbol * E.ty) list)
fun addForAllBinding (s, ty) = let
val newName = getNewName (s, !used)
in
used := (!used <+ newName);
forallbindings := (newName, ty) :: !forallbindings;
newName
end
fun conv (env, e as E.BinBoolExpr {left, bop, right, ...}) = let
(*{{{1*)
val (l, r) = (conv (env, left), conv (env, right))
in case (l, r, bop)
of (Term (NonClock le), Term (NonClock re), _)=> Term (NonClock e)
| (Term (NonClock le), _, E.ImplyOp) => Or (negate l, r)
| (_, _, E.ImplyOp) => raise NonClockTerm
| (_, _, E.OrOp) => Or (l, r)
| (_, _, E.AndOp) => And (l, r)
end
(* possibly: c1 - c2 {<,<=,==,>=,>} e *)
| conv (env, e as E.RelExpr {left=E.BinIntExpr
{left=lclk, bop=E.MinusOp, right=rclk, ...},
rel, right, ...}) =
if isClkVar (env, lclk) andalso isClkVar (env, rclk)
then Term (CDiff (toVar lclk, toVar rclk, toRel rel, toVal right))
else notClk (env, e)
| conv (env, e as E.RelExpr {right=E.BinIntExpr
{left=lclk, bop=E.MinusOp, right=rclk, ...},
rel, left, ...}) =
if isClkVar (env, lclk) andalso isClkVar (env, rclk)
then Term (CDiff (toVar lclk, toVar rclk, toFlipRel rel, toVal left))
else notClk (env, e)
(* possibly: c {<,<=,==,>=,>} e *)
| conv (env, e as E.RelExpr {left, rel, right, ...}) = let in
case (isClkVar (env, left), isClkVar (env, right))
of (true, true) => raise NonClockTerm
| (false, false) => Term (NonClock e)
| (true, false) => Term (CRel (toVar left,toRel rel,toVal right))
| (false, true) => Term (CRel (toVar right, toFlipRel rel,
toVal left))
end
| conv (env, e as E.VarExpr v) = if isClk (env, v) then raise NonClockTerm
else Term (NonClock e)
(* Guard must be side-effect free *)
| conv (env, E.UnaryModExpr _) = raise NonClockTerm
| conv (env, E.Deadlock _) = raise NonClockTerm
| conv (env, e as E.IntCExpr _) = Term (NonClock e)
| conv (env, e as E.BoolCExpr _) = Term (NonClock e)
| conv (env, e as E.AssignExpr _) = notClk (env, e)
| conv (env, e as E.NegExpr _) = notClk (env, e)
| conv (env, e as E.NotExpr _) = notClk (env, e)
| conv (env, e as E.BinIntExpr _) = notClk (env, e)
| conv (env, e as E.CallExpr {args, ...}) = notClk (env, e)
(* tested in Uppaal 4.0.2: (i==1)?(x>2):(x>3) //int i, clock x;
gives: incompatible arguments to inline if *)
| conv (env, e as E.CondExpr _) = notClk (env, e)
| conv (env, e as E.ForAllExpr {id,ty,expr,...}) = let
val env' = Env.addId Env.BoundScope ((id, ty), env)
in
if containsClocks (env', expr)
then let (* lift forall to top-level, i.e. make prenex
the usual proviso on names must be respected *)
val id' = addForAllBinding (id, ty)
in
conv (Env.addId Env.BoundScope ((id', ty), env),
E.renameVar ({old=id, new=id'}, expr))
end
else Term (NonClock e)
end
| conv (env, e as E.ExistsExpr _) = notClk (env, e)
(*}}}1*)
in (conv (env, expr), !forallbindings, !used) end
end (* local *)
local
(*{{{1*)
fun fromCRel Lt = E.LtOp | fromCRel Leq = E.LeOp
| fromCRel Geq = E.GeOp | fromCRel Gt = E.GtOp
| fromCRel Eq = E.EqOp
fun fromCVal (Simple i) = E.IntCExpr i
| fromCVal (Complex e) = e
fun fromClkT (NonClock e) = e
| fromClkT (CRel (v, rel, cv)) = E.RelExpr {left=E.VarExpr v,
rel=fromCRel rel,
right=fromCVal cv,
pos=E.nopos}
| fromClkT (CDiff (v1, v2, rel, cv)) = let
val d = E.BinIntExpr {left=E.VarExpr v1,
bop=E.MinusOp,
right=E.VarExpr v2,
pos=E.nopos}
in
E.RelExpr {left=d, rel=fromCRel rel,
right=fromCVal cv, pos=E.nopos}
end
(*}}}1*)
in
fun toExpr (t, fas) = let
fun toE (Term ct) = fromClkT ct
| toE (And (ce1, ce2)) = E.BinBoolExpr {left=toE ce1, bop=E.AndOp,
right=toE ce2, pos=E.nopos}
| toE (Or (ce1, ce2)) = E.BinBoolExpr {left=toE ce1, bop=E.OrOp,
right=toE ce2, pos=E.nopos}
fun wrapForall ((s, ty), e)=E.ForAllExpr {id=s,ty=ty,expr=e,pos=E.nopos}
in foldl wrapForall (toE t) fas end
end (* local *)
(* see tech. report: canswap predicate *)
fun conflictExists (sE, sA, psi) = let
exception ConflictingQuantifiers
fun termToPairs ct = let
val f = getTermFree ct
val e = AtomSet.intersection (f, sE)
val a = AtomSet.intersection (f, sA)
in
if not (AtomSet.isEmpty e) andalso not (AtomSet.isEmpty a)
then raise ConflictingQuantifiers else (e, a)
end
fun pairUnion ((e1,a1), (e2,a2)) = (e1 ++ e2, a1 ++ a2)
val emptyPair = (emptyset, emptyset)
fun findCommon ((e,a), (se,sa)) = let
val ei = if AtomSet.isEmpty a then se ++ e else se
val ai = if AtomSet.isEmpty e then sa ++ a else sa
in (ei, ai) end
val termPairs = map (fn cl=>map termToPairs cl) psi
(* [ [(E,A), ..., (E,A)], ..., [(E,A), ..., (E,A)] ] *)
val clausePairs = map (fn cl=>foldl pairUnion emptyPair cl) termPairs
(* [ (E,A), ..., (E,A) ] *)
val (sEf, sAf) = foldl findCommon emptyPair clausePairs
fun conflict ([], _) = false
| conflict ((e, a)::xs, (confE, confA)) =
if (AtomSet.isSubset (e, sEf) andalso AtomSet.isEmpty (a))
orelse (AtomSet.isSubset (a, sAf) andalso AtomSet.isEmpty (e))
then conflict (xs, (confE, confA))
else if not (AtomSet.isEmpty (AtomSet.intersection (e, confE)))
orelse not (AtomSet.isEmpty (AtomSet.intersection (a, confA)))
then true else conflict (xs, (confE ++ e, confA ++ a))
in conflict (clausePairs, (sEf, sAf)) end
handle ConflictingQuantifiers => true
local (*{{{1*)
datatype termchoice =
KeepLeft (* M |- (l && r) <=> M |- l *)
| KeepRight (* M |- (l && r) <=> M |- r *)
| MergeEqual (* M |- (le >= c && re <= c) <=> M |- (le = c) *)
| Contra (* M |- (l && r) <==> M |- false *)
| KeepBoth (* none of the above *)
(* Guards are integer-valued, but the clocks themselves are real-valued. *)
fun chooseFromSimpleRel ((Lt, i), r) = (case r
of (Lt , j) => if i <= j then KeepLeft else KeepRight
| (Leq, j) => if i <= j then KeepLeft else KeepRight
| (Eq , j) => if i > j then KeepRight else Contra
| (Geq, j) => if i > j then KeepBoth else Contra
| (Gt , j) => if i > j then KeepBoth else Contra
)
| chooseFromSimpleRel ((Leq, i), r) = (case r (*{{{2*)
of (Lt , j) => if i < j then KeepLeft else KeepRight
| (Leq, j) => if i < j then KeepLeft else KeepRight
| (Eq , j) => if i >= j then KeepRight else Contra
| (Geq, j) => if i = j then MergeEqual else
if i > j then KeepBoth else Contra
| (Gt , j) => if i > j then KeepBoth else Contra
)
| chooseFromSimpleRel ((Eq , i), r) = (case r
of (Lt , j) => if i < j then KeepLeft else Contra
| (Leq, j) => if i <= j then KeepLeft else Contra
| (Eq , j) => if i = j then KeepLeft else Contra
| (Geq, j) => if i >= j then KeepLeft else Contra
| (Gt , j) => if i > j then KeepLeft else Contra
)
| chooseFromSimpleRel ((Geq, i), r) = (case r
of (Lt , j) => if i < j then KeepBoth else Contra
| (Leq, j) => if i = j then MergeEqual else
if i < j then KeepBoth else Contra
| (Eq , j) => if i <= j then KeepRight else Contra
| (Geq, j) => if i > j then KeepLeft else KeepRight
| (Gt , j) => if i > j then KeepLeft else KeepRight
)
| chooseFromSimpleRel ((Gt , i), r) = (case r
of (Lt , j) => if i < j then KeepBoth else Contra
| (Leq, j) => if i < j then KeepBoth else Contra
| (Eq , j) => if i < j then KeepRight else Contra
| (Geq, j) => if i >= j then KeepLeft else KeepRight
| (Gt , j) => if i >= j then KeepLeft else KeepRight
(*}}}2*) )
(* Handle ((el1 ~1 er1) && (el2 ~2 er2)) with el1=er1, er1=er2: *)
fun chooseFromComplexRel (Lt , r) = (case r of Lt => KeepLeft
| Leq => KeepLeft
| _ => Contra)
| chooseFromComplexRel (Leq, r) = (case r of Geq => MergeEqual (*{{{2*)
| Gt => Contra
| _ => KeepRight)
| chooseFromComplexRel (Eq , r) = (case r of Lt => Contra
| Gt => Contra
| _ => KeepLeft)
| chooseFromComplexRel (Geq, r) = (case r of Leq => MergeEqual
| Lt => Contra
| _ => KeepRight)
| chooseFromComplexRel (Gt , r) = (case r of Gt => KeepLeft
| Geq => KeepLeft
(*}}}2*) | _ => Contra)
fun chooseTerm (CRel (c1, rel1, Simple i1),
CRel (c2, rel2, Simple i2))
= if E.varequal (c1, c2)
then chooseFromSimpleRel ((rel1, i1), (rel2, i2))
else KeepBoth
(*{{{2*)
| chooseTerm (CRel (c1, rel1, Complex e1),
CRel (c2, rel2, Complex e2))
= if E.varequal (c1, c2) andalso E.equal (e1, e2)
then chooseFromComplexRel (rel1, rel2)
else KeepBoth
| chooseTerm (CDiff (cl1, cr1, rel1, Simple i1),
CDiff (cl2, cr2, rel2, Simple i2))
= if E.varequal (cl1, cl2) andalso E.varequal (cr1, cr2)
then chooseFromSimpleRel ((rel1, i1), (rel2, i2))
else KeepBoth
| chooseTerm (CDiff (cl1, cr1, rel1, Complex e1),
CDiff (cl2, cr2, rel2, Complex e2))
= if E.varequal (cl1, cl2) andalso E.varequal (cr1, cr2)
andalso E.equal (e1, e2)
then chooseFromComplexRel (rel1, rel2) else KeepBoth
| chooseTerm (NonClock(E.BoolCExpr b),_)= if b then KeepRight else Contra
| chooseTerm (_,NonClock(E.BoolCExpr b)) = if b then KeepLeft else Contra
| chooseTerm (NonClock e1, NonClock e2)
= if E.isNegation (e1, e2) then Contra else KeepBoth
| chooseTerm _ = KeepBoth
(*}}}2*)
exception Contradiction
fun termAndConj (t, cs) = let
fun mergeEqual (CRel (c, _, v)) = CRel (c, Eq, v)
| mergeEqual (CDiff (c1, c2, _, v)) = CDiff (c1, c2, Eq, v)
fun tandc (rs, t, []) = t::rs
| tandc (rs, t, x::xs) = case chooseTerm (t, x)
of KeepLeft => tandc (rs, t, xs)
| KeepRight => List.revAppend (rs, x::xs)
| MergeEqual => List.revAppend (rs, mergeEqual t::xs)
| Contra => raise Contradiction
| KeepBoth => tandc (x::rs, t, xs)
in tandc ([], t, cs) end
fun conjAndConj and1 and2 = SOME (foldl termAndConj and2 and1)
handle Contradiction => NONE
fun andDNFLists (or1, or2) = let
fun throughSecond andx = let
val r = List.mapPartial (conjAndConj andx) or2
in if null r then NONE else SOME r end
in
List.concat (List.mapPartial throughSecond or1)
end
(*}}}1*)
in
fun toDNF (Term ct) = [[ct]]
| toDNF (Or (e1, e2)) = toDNF e1 @ toDNF e2
| toDNF (And (e1, e2)) = andDNFLists (toDNF e1, toDNF e2)
end (* local *)
fun fromDNF xxs = let
fun combineAnd (t, e) = And (e, Term t)
fun makeAnd [] = NONE
| makeAnd (x::xs) = SOME (foldl combineAnd (Term x) xs)
fun combineOr (e1, e2) = Or (e2, e1)
fun makeOr [] = Term (NonClock (E.falseExpr))
| makeOr (x::xs) = foldl combineOr x xs
fun trueExpr (Term (NonClock t)) = E.equal (t, E.trueExpr)
| trueExpr _ = false
val andclauses = List.mapPartial makeAnd xxs
in if List.exists trueExpr andclauses
then Term (NonClock (E.trueExpr))
else makeOr andclauses
end
fun andexpr (e1, e2) = fromDNF (toDNF (And (e1, e2)))
(* exploit the simplification built into toDNF *)
end
end