| Line 1... |
Line 1... |
(* $Id: clkexprtrans.sml 47 2008-05-11 05:46:38Z tbourke $ *)
|
(* $Id: clkexprtrans.sml 49 2008-07-21 07:02:40Z tbourke $ *)
|
|
|
(* TODO:
|
(* TODO:
|
* - rename `paritition' to `constraint'
|
* - rename `paritition' to `constraint'
|
* more generally it is used to constrain the applicability of
|
* more generally it is used to constrain the applicability of
|
* a set of transitions and is not affected by negation.
|
* a set of transitions and is not affected by negation.
|
| Line 63... |
Line 63... |
(fn (s, str)=> str ^ " " ^ Atom.toString s) "" names ^
|
(fn (s, str)=> str ^ " " ^ Atom.toString s) "" names ^
|
" }\n"
|
" }\n"
|
end
|
end
|
end (* local *)
|
end (* local *)
|
|
|
(*
|
|
(*TODO: DEBUG ONLY! *)
|
|
fun showPartitions showitem partitions = let
|
|
fun showClass c = let in
|
|
TextIO.print " class[\n";
|
|
map showitem c;
|
|
TextIO.print " class]\n"
|
|
end
|
|
|
|
fun showPart p = let in
|
|
TextIO.print "partition[\n";
|
|
map showClass p;
|
|
TextIO.print "partition]\n"
|
|
end
|
|
in app showPart partitions end
|
|
*)
|
|
|
|
fun unionNames cetrans = let
|
fun unionNames cetrans = let
|
fun f (CETrans {names, ...}, m) = m ++ names
|
fun f (CETrans {names, ...}, m) = m ++ names
|
in foldl f emptyset cetrans end
|
in foldl f emptyset cetrans end
|
|
|
fun fromATrans preenv (AT.ActTrans {selectids=sellist,
|
fun fromATrans preenv (AT.ActTrans {selectids=sellist,
|
| Line 203... |
Line 186... |
fun negate (cinv_fall, cinv)
|
fun negate (cinv_fall, cinv)
|
(cet as CETrans {actselect, gselect, forall, guard,
|
(cet as CETrans {actselect, gselect, forall, guard,
|
partition, action, names}) =
|
partition, action, names}) =
|
let
|
let
|
val g' = ClkE.negate guard
|
val g' = ClkE.negate guard
|
val e = case cinv of
|
val (e, tnone) = case (ClkE.isConstant g', ClkE.isConstant cinv) of
|
ClkE.Term (ClkE.NonClock (E.BoolCExpr true)) => g'
|
(SOME true, SOME true) => (ClkE.trueExpr, false)
|
| _ => ClkE.And (cinv, g')
|
| (SOME true, _) => (cinv, false)
|
|
| (_, SOME true) => (g', false)
|
|
| (NONE, NONE) => (ClkE.And (cinv,g'),false)
|
|
| _ => (ClkE.falseExpr, true)
|
val dnf = ClkE.toDNF e
|
val dnf = ClkE.toDNF e
|
|
|
val _ = Util.debugVeryDetailed (fn()=>["* CETrans.negate before:\n",
|
val _ = Util.debugVeryDetailed (fn()=>["* CETrans.negate before:\n",
|
toString cet])
|
toString cet])
|
|
|
| Line 217... |
Line 203... |
fun addAndCheck ((n, _), s) = if n <- s
|
fun addAndCheck ((n, _), s) = if n <- s
|
then raise Fail "addDisjointForalls"
|
then raise Fail "addDisjointForalls"
|
else s <+ n
|
else s <+ n
|
val _ = foldl addAndCheck (ClkE.getFree g') cinv_fall
|
val _ = foldl addAndCheck (ClkE.getFree g') cinv_fall
|
in
|
in
|
|
if tnone then [] else (* guard was false *)
|
if ClkE.conflictExists (addNameTypes gselect, addNameTypes forall, dnf)
|
if ClkE.conflictExists (addNameTypes gselect, addNameTypes forall, dnf)
|
then raise SelectIdConflictsWithForAll (#1 (ListPair.unzip gselect),
|
then raise SelectIdConflictsWithForAll (#1 (ListPair.unzip gselect),
|
#1 (ListPair.unzip forall))
|
#1 (ListPair.unzip forall))
|
else let
|
else let
|
val (trans, fall)=ListPair.unzip (map
|
val (trans, fall)=ListPair.unzip (map
|
| Line 240... |
Line 227... |
else (Util.warn ["forall bindings ",
|
else (Util.warn ["forall bindings ",
|
ListFormat.fmt {init="(", sep=", ", final=")",
|
ListFormat.fmt {init="(", sep=", ", final=")",
|
fmt=Atom.toString}
|
fmt=Atom.toString}
|
(AtomSet.listItems splitFAlls),
|
(AtomSet.listItems splitFAlls),
|
" are shared across disjuncts: possible split zones"];
|
" are shared across disjuncts: possible split zones"];
|
|
(* TODO: increase the accuracy of this detection
|
|
* and implement the construction from
|
|
* thesis chapter to handle them. *)
|
[CETrans {actselect=actselect,
|
[CETrans {actselect=actselect,
|
gselect=forall,
|
gselect=forall,
|
forall=gselect @ cinv_fall,
|
forall=gselect @ cinv_fall,
|
partition=partition,
|
partition=partition,
|
guard=e,
|
guard=e,
|
guard=e,
|
guard=e,
|