[/] [trunk/] [src/] [maketest/] [transitionflipper.sml] - Rev 62
(* $Id: transitionflipper.sml 62 2008-08-20 11:20:33Z tbourke $
*
* Copyright (c) 2008 Timothy Bourke (University of NSW and NICTA)
* All rights reserved.
*
* This program is free software; you can redistribute it and/or modify it
* under the terms of the "BSD License" which is distributed with the
* software in the file LICENSE.
*
* This program is distributed in the hope that it will be useful, but
* WITHOUT ANY WARRANTY; without even the implied warranty of
* MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE. See the BSD
* License for more details.
*)
(*TODO:
* Check whether duplicate selectids can muck things up.
* Remove unused select ids from final transitions (or initial transitions?).
fun removeEarlierDuplicates l = let (* there can be only one *)
fun p s (s', _) = not (s =:= s')
fun f [] = []
| f ((x as (s, _))::xs) = x :: f (List.filter (p s) xs)
in rev (f (rev l)) end
fun unusedId used (E.BoundId (s, ty)) = if s <- used
then SOME (s, ty) else NONE
val sellist = removeEarlierDuplicates
(List.mapPartial (unusedId (!usednames)) presellist)
* What happens if we call negate(negate tr)?
Should this be forbidden by using types?
* Should check whether any actselect indices are used in guard terms in a way
that will create problems (restrict how actions are selected?).
e.g. select i . (i > 4) / a[i]
||negate
\/
select i . (i <= r) / a[i]
But how would this combine with other transitions? Does it work?
This must first be understood properly.
* What about action selectids with non-zero lower bounds?
chan c[6];
select i : int[2,5] . true / c[i]
Either forbid, or the negation set has to include:
select i : int [0,1] . true / c[i]
* Need a mapping back from scalar sets to their typedef-ed names (possibly via
uniqueid lookup?, or don't expand to begin with (would this break anything
else?). See tests/testflip13, the selectid should come from 'S', not
scalar[5].
*)
structure TransitionFlipper :> TRANSITION_FLIPPER = let
structure E = Expression
and Env = Environment
and ECVT = ExpressionCvt
and ATrans = ActionTrans
and STrans = SelTrans
and ClkE = ClockExpression
and CETrans = ClkExprTrans
in struct
exception FlipFailed of string
(* shortcuts over Atom and AtomSet *)
infix <+ <- ++ <\ \ =:= ; open Symbol
type t = {selectids: E.boundid list,
actionsubs: E.expr list,
guard: E.expr}
fun toString {selectids, actionsubs, guard} = let
fun showActions [] = ""
| showActions (e::es) = "[" ^ ECVT.Expr.toString e ^"]"^ showActions es
fun boundToStr (E.BoundId (s, ty)) = Atom.toString s ^
" : " ^ ECVT.Ty.toString ty
val bindingList = (ListFormat.fmt {init="(", sep=", ",
final=")", fmt=boundToStr})
in
"{select: " ^ bindingList selectids ^ "\n" ^
" action: " ^ showActions actionsubs ^ "\n " ^
" guard: " ^ ECVT.Expr.toString guard ^ " }" ^ "\n"
end
local
fun convBind (E.BoundId (nm, ty), (xs,used)) = ((nm, ty)::xs, used <+ nm)
in
fun andexpr env (ce1se, e1, e2) = let
val (ce1se', used) = foldl convBind ([], emptyset) ce1se
val (ce1, ce1fa, used) = ClkE.fromExpr (used, env, e1)
val (ce2, ce2fa, _ ) = ClkE.fromExpr (used, env, e2)
val (ce2fa', ce2') = ClkE.ensureNoBindingConflict (ce1fa @ ce1se',ce1)
(ce2fa,ce2)
in ClkE.toExpr (ClkE.andexpr (ce1, ce2'), ce1fa @ ce2fa') end
end (* local *)
fun negateInvariant env invExpr = let
val _ = Util.debugIndent (Settings.Outline,fn()=>["=negateInvariant="])
val atr = ActionTrans.fromTrans []
{selectids=[], actionsubs=[], guard=invExpr}
val ctr = (CETrans.fromATrans env) atr
val _ = Util.debugDetailed (fn ()=>["* before:\n", CETrans.toString ctr])
val ctrs' = CETrans.negate ([], ClkE.trueExpr) ctr
val _ = Util.debugDetailed (fn ()=> "* after:\n"
::map (fn c=>CETrans.toString c ^"\n") ctrs')
in
map CETrans.toTrans ctrs'
before (Util.debugOutdent (Settings.Outline, fn()=>[]))
end
handle ClkE.NonClockTerm => raise FlipFailed "bad clock terms in invariant"
(* XXX: partitioning technique *)
fun negatePartitionedTransitions env (subtypes, trans : t list, invariant) =
let
val _ = Util.debugIndent (Settings.Outline,fn()=>["=negatePartitioned="])
val _ = Util.debugDetailed (fn ()=>map toString trans)
(* 1. Group like subscripts; rename subSelectIds; make others unique. *)
val atrans = ATrans.ensureConsistency
(map (ATrans.fromTrans subtypes) trans)
val otherATrans = ATrans.coverMissingChannels (subtypes, atrans,
invariant)
val atrans' = map (ATrans.reduceSelectIds env) atrans
val cetrans = map (CETrans.fromATrans env) atrans'
val _ = Util.debugSubsect (Settings.Outline, fn()=>
["* cover missing channels:",
if null otherATrans then " nothing" else "\n"]
@ map ATrans.toString otherATrans)
(* 2. Paritition remaining transitions. *)
val partitions = Partitions.makeList cetrans
(* 3. Form partition expressions: just over freeSubscripts
Grouping back into a single list of transitions. *)
val cetrans = List.concat (List.map CETrans.formPartitionReps partitions)
val _ = Util.debugDetailed (fn ()=>
["* with partition reps:", if null cetrans then " nothing" else "\n"]
@ map CETrans.toString cetrans)
(* 4. Convert the location invariant into a clock expression *)
val (cinv, cinv_fall, _) = ClkE.fromExpr (CETrans.unionNames cetrans,
env, invariant)
(* 5. Negate each, concatenating results. *)
val ncetrans = List.concat (List.map (CETrans.negate (cinv_fall, cinv))
cetrans)
val _ = Util.debugDetailed (fn ()=>
["* after negation:", if null ncetrans then " nothing" else "\n"]
@ map CETrans.toString ncetrans)
in map ATrans.toTrans otherATrans @ map CETrans.toTrans ncetrans
before (Util.debugOutdent (Settings.Outline, fn()=>[]))
end
handle CETrans.SelectIdConflictsWithForAll (sel, forall) => let
fun showSym n = ListFormat.fmt {init=n ^ "(", final=")",
sep=", ", fmt=Atom.toString}
in
raise FlipFailed ("select/forall conflict, " ^
showSym "select" sel ^
showSym "forall" forall )
end
| ClkE.NonClockTerm => raise FlipFailed "bad clock terms in guard"
| ATrans.ActSubWithNonSimpleSelect e => raise FlipFailed (
"channel subscript contains non-simple bound variable (" ^
ExpressionCvt.Expr.toString e ^ ")")
| ATrans.ActSubWithBadType {expr, badty, goodty} => raise FlipFailed
("channel subscript select variable " ^
ExpressionCvt.Expr.toString expr ^ " has type " ^
ExpressionCvt.Ty.toString badty ^ ", not " ^
ExpressionCvt.Ty.toString goodty)
| ATrans.BadSubscriptCount =>
raise FlipFailed ("wrong number of channel subscripts")
| ATrans.MixedSubscriptTypes (e1, e2) => raise FlipFailed
("non-consistent channel subscript dimensions (" ^
ExpressionCvt.Expr.toString e1 ^ ", " ^
ExpressionCvt.Expr.toString e2 ^ ")")
fun negateTransitions env (subtypes, trans : t list, invariant) = let
val _ = Util.debugIndent (Settings.Outline,fn()=>["=negateTransitions="])
val _ = Util.debugDetailed (fn ()=>map toString trans)
(* 1. Group like subscripts; rename subSelectIds; make others unique. *)
val subIdx = ListPair.zip
(STrans.makeIndexNames (length subtypes) trans, subtypes)
val strans = map (STrans.fromTrans subIdx) trans
val mstrans = STrans.mergeTrans strans
val _ = Util.debugVeryDetailed (fn()=>["* after merging:\n",
STrans.toString subIdx mstrans])
val cetran = CETrans.fromSTrans env subIdx mstrans
(* 2. Convert the location invariant into a clock expression *)
val (cinv, cinv_fall, _) = ClkE.fromExpr (CETrans.unionNames [cetran],
env, invariant)
(* 3. Negate the transition. *)
val ncetrans = CETrans.negate (cinv_fall, cinv) cetran
val _ = Util.debugDetailed (fn ()=>
["* after negation:", if null ncetrans then " nothing" else "\n"]
@ map CETrans.toString ncetrans)
in map CETrans.toTrans ncetrans
before (Util.debugOutdent (Settings.Outline, fn()=>[]))
end
handle CETrans.SelectIdConflictsWithForAll (sel, forall) => let
fun showSym n = ListFormat.fmt {init=n ^ "(", final=")",
sep=", ", fmt=Atom.toString}
in
raise FlipFailed ("select/forall conflict, " ^
showSym "select" sel ^
showSym "forall" forall )
end
| ClkE.NonClockTerm => raise FlipFailed "bad clock terms in guard"
| STrans.NonSimpleSelectIndex e => raise FlipFailed (
"channel subscript contains non-simple bound variable (" ^
ExpressionCvt.Expr.toString e ^ ")")
| STrans.BadChannelIndex {id, badty, goodty} => raise FlipFailed
("channel subscript select variable " ^
Atom.toString id ^ " has type " ^
ExpressionCvt.Ty.toString badty ^ ", not " ^
ExpressionCvt.Ty.toString goodty)
| STrans.BadSubscriptCount =>
raise FlipFailed ("wrong number of channel subscripts")
fun chanToSubRanges (env, s) = let
fun arrToList (E.CHANNEL _, r) = SOME r
| arrToList (E.ARRAY (ty, E.Type sub), r) = arrToList (ty, sub::r)
| arrToList _ = NONE
in
Option.composePartial (fn ty=> arrToList (ty, []), Env.findValType env) s
end
end
end