Compare Revisions

This comparison shows the changes necessary to convert path /trunk/src/maketest from Rev 43 to Rev 44 (Reverse comparison).
Path Comparison

Rev 43 ⟶ Rev 44

/sources.cm
13,6 ⟶ 13,10
 
action_trans.sig
actiontrans.sml
 
sel_trans.sig
seltrans.sml
 
clock_expression.sig
clockexpression.sml
clk_expr_trans.sig
/seltrans.sml
New file
0,0 ⟶ 1,290
(* $Id$ *)
 
structure SelTrans :> SEL_TRANS = let
structure E = Expression
and ECVT = ExpressionCvt
and Env = Environment
in struct
type expr = Expression.expr
and ty = Expression.ty
and symbol = Atom.atom
and symbolset = AtomSet.set
 
exception NonSimpleSelectIndex of expr
exception BadChannelIndex of {id: symbol, badty: ty, goodty: ty}
exception BadSubscriptCount
 
infix <+ <- ++ <\ \ =:= ; open Symbol
 
datatype t = SelTrans of {selectids: (symbol * ty) list,
guard: expr,
names: symbolset}
 
(* utility functions for processing names *)
fun toBoundId (s, ty) = E.BoundId (s, ty)
fun fromBoundId (E.BoundId (n, ty)) = (n, ty)
 
fun addNameTypes xs = let
fun add ((n, _), s) = s <+ n
in foldl add emptyset xs end
 
fun addBoundId (E.BoundId (n, _), s) = s <+ n
fun addExprIds (e, s) = s ++ (E.getFreeNames e)
 
fun tnames ({selectids, actionsubs, guard}, (sels, gs)) =
(foldl addBoundId sels selectids,
foldl addExprIds (addExprIds (guard, gs)) actionsubs)
 
local
(*{{{1*)
fun selActionSubs {selectids, actionsubs, guard} = actionsubs
 
fun transpose isSelBinding = let
fun cons (e, gs) = case isSelBinding e of
NONE => gs
| SOME s => s::gs
fun f ([], gss) = gss
| f (e::es, []) = cons (e, [])::f (es, [])
| f (e::es, gs::gss) = cons (e, gs)::f (es, gss)
in f end
 
fun selNames ([n], (xs, used)) = if n <- used
then let val n' = getNewName (n, used)
in (n'::xs, used <+ n') end
else (n::xs, used <+ n)
| selNames (n::ns, (xs, used)) = if n <- used
then selNames (ns, (xs, used))
else (n::xs, used <+ n)
| selNames ([], _) = raise Fail "Fault in SelTrans.makeIndexNames"
(*}}}1*)
in
fun makeIndexNames n ts = let
val (selNms, gs) = foldl tnames (emptyset, emptyset) ts
val gNms = gs \ selNms
 
fun isSel (E.VarExpr (E.SimpleVar s)) = if s <- selNms
then SOME s else NONE
| isSel _ = NONE
 
val defaults = List.tabulate (n, fn i => [`("s" ^ Int.toString i)])
val potNames = List.take (foldl (transpose isSel)
defaults
(map selActionSubs ts), n)
in #1 (foldl selNames ([], gNms) potNames) end
end (* local *)
 
local (*{{{1*)
fun symtyToStr (s, ty) = Atom.toString s ^ " : " ^ ECVT.Ty.toString ty
val symtyList = (ListFormat.fmt {init="(", sep=", ",
final=")", fmt=symtyToStr})
in (*}}}1*)
fun toString actidx (SelTrans {selectids, guard, names}) = let in
"{selectids: " ^ symtyList selectids ^ "\n" ^
" guard: " ^ ECVT.Expr.toString guard ^ "\n" ^
" actidx: " ^ symtyList actidx ^ "\n" ^
" names: " ^ AtomSet.foldl
(fn (s, str)=> str ^ " " ^ Atom.toString s) "" names ^
" }\n"
end
end (* local *)
 
local
(*{{{1*)
fun addBoundTyMap (E.BoundId (n, ty), m) = AtomMap.insert (m, n, ty)
 
fun names ({selectids, actionsubs, guard}, (sels, gs)) =
(foldl addBoundId sels selectids,
foldl addExprIds (addExprIds (guard, gs)) actionsubs)
 
fun equate (l, r) = E.RelExpr {left=l, rel=E.EqOp, right=r}
 
fun limit (nm, rel, limit) = E.RelExpr {left=E.VarExpr (E.SimpleVar nm),
rel=rel, right=limit}
 
(* matchSelRange (selid, actualRange, selectedRange) *)
fun matchSelRange (_, E.INT(NONE, E.NoQual),
E.INT(NONE, E.NoQual)) = SOME NONE
| matchSelRange (nm, E.INT (SOME (lRan, uRan), E.NoQual),
E.INT (SOME (lSel, uSel), E.NoQual)) =
SOME (case (E.equal (lSel, lRan), E.equal (uSel, uRan)) of
(true, true) => NONE
| (true, false) => SOME (limit (nm, E.LeOp, uSel))
| (false, true) => SOME (limit (nm, E.GeOp, lSel))
| (false, false) => SOME (E.BinBoolExpr{bop=E.AndOp,
left=limit (nm,E.GeOp,lSel),right=limit (nm,E.LeOp,uSel)}))
 
| matchSelRange (nm, E.NAME (_, E.NoQual, SOME tyex1),
E.NAME (_, E.NoQual, SOME tyex2))
= matchSelRange (nm, tyex1, tyex2)
| matchSelRange (nm, ty1, E.NAME (_, E.NoQual, SOME tyex2))
= matchSelRange (nm, ty1, tyex2)
| matchSelRange (nm, E.NAME (_, E.NoQual, SOME tyex1), ty2)
= matchSelRange (nm, tyex1, ty2)
 
| matchSelRange (_, E.NAME (s1, E.NoQual, _), E.NAME (s2, E.NoQual, _)) =
if s1 =:= s2 then SOME NONE else NONE
 
| matchSelRange (_, ty1, ty2) = if E.tyequal (ty1, ty2)
then SOME NONE else NONE
 
(* addLimitClause (selid, actualRange, selectedRange, guard) *)
fun addLimitClause (n, ty, ty', g) =
case matchSelRange (n, ty, ty') of
SOME NONE => g
| SOME (SOME c) => E.andexpr (g, c)
| NONE => raise BadChannelIndex {id=n, badty=ty', goodty=ty}
 
(* Assumption:
* Each of the newidx values will have a different prefix (e.g. s0, s1,...)
* and the getNewName function returns a new name based on the given prefix
* so there will never be a clash even if we don't update the set of used
* names. *)
fun makeMap isSelBinding used = let
fun f (((newidx, _), e), map) = let
val map' = AtomMap.insert (map, newidx, getNewName (newidx, used))
in
case isSelBinding e of
NONE => map'
| SOME s => if s =:= newidx then map'
else AtomMap.insert (map, s, newidx)
end
in f end
 
fun zip (x::xs, y::ys) = (x, y):: zip (xs, ys)
| zip ([], []) = []
| zip _ = raise BadSubscriptCount
 
fun toVar s = E.VarExpr (E.SimpleVar s)
 
(*}}}1*)
in
fun fromTrans actids (ts as {selectids, actionsubs, guard}) = let
val idxSeqs = zip (actids, actionsubs)
val (selNms, gs) = tnames (ts, (addNameTypes actids, emptyset))
 
val sidTypes = foldl addBoundTyMap AtomMap.empty selectids
 
fun isSel (E.VarExpr (E.SimpleVar s)) = if s <- selNms
then SOME s else NONE
| isSel _ = NONE
 
val renMap = foldl (makeMap isSel (selNms ++ gs)) AtomMap.empty idxSeqs
 
fun changeIdxs (((newidx, newty), e), (selids, g, prevUse)) =
let
fun varIsSel (env, E.VarExpr (E.SimpleVar s)) =
(case Env.findValScope env s of
NONE => s <- selNms
| SOME BoundScope => false)
| varIsSel _ = false
 
fun containsSel e = null (Env.filter varIsSel Env.base_env e)
in
case isSel e of
(* for a selectid i
* -if the type doesn't cover the whole dimension then && in a
* restriction clause (l <= s_i <= u) where i has the type int[l,u]
* -if used in an earlier index, s_j, then && the clause (s_i == s_j)
* -if doesn't match the current name then rename (s_i/i)
* -remove i from the list of selectids *)
SOME s => let
val g' = addLimitClause (newidx,
Option.valOf (AtomMap.find (sidTypes, s)),
newty, g)
val g'' = case AtomMap.find (prevUse, s) of
NONE => g'
| SOME s' => let
val c = equate (toVar newidx, toVar s')
in E.andexpr (g', c) end
 
fun skip_s (E.BoundId (nm, ty)) = if s =:= nm then NONE
else SOME (nm, ty)
in
(List.filter (fn (nm, _)=> not (s =:= nm)) selids,
E.renameVar ({old=s, new=newidx}, g''),
AtomMap.insert (prevUse, s, newidx))
end
 
(* for a state expression e:
* -throw an exception if it contains selectids
* -&& the clause (si == R'(e)) to the guard *)
| NONE => if containsSel e then raise NonSimpleSelectIndex e
else let
val c= equate (toVar newidx, E.renameVars renMap e)
in (selids, E.andexpr (g, c), prevUse) end
end (* changeIdxs *)
 
val (selids, g, _) = foldl changeIdxs
(map fromBoundId selectids, guard, AtomMap.empty)
idxSeqs
in
SelTrans
{selectids=selids,
guard=g,
names=(foldl (fn ((n, _), s) => s <+ n) (E.getFreeNames g) selids)}
end
end (* local *)
 
 
fun toTrans actids (SelTrans {selectids, guard, ...}) =
{selectids=map toBoundId selectids @ map toBoundId actids,
actionsubs=map (fn (nm,_)=> E.VarExpr (E.SimpleVar nm)) actids,
guard=guard}
 
local
(*{{{1*)
fun merge (SelTrans {selectids=sids1, guard=g1, names=names1},
SelTrans {selectids=sids2, guard=g2, names=names2}) =
let
fun f ((s as (nm, ty)), (selects, rename, used)) =
if nm <- names2
then let val nm' = getNewName (nm, used)
in
((nm', ty)::selects,
AtomMap.insert (rename, nm, nm'),
used <+ nm')
end
else (s::selects, rename, used)
 
val (selects, rename, used) =
foldl f ([], AtomMap.empty, names1 ++ names2) sids1
in
SelTrans {selectids=List.revAppend (selects, sids2),
guard=E.orexpr (E.renameVars rename g1, g2),
names=used}
end
(*}}}1*)
in
fun mergeTrans [] = SelTrans {selectids=[],
guard=E.falseExpr,
names=emptyset}
| mergeTrans [x] = x
| mergeTrans (x1::x2::xs) = mergeTrans (merge (x1, x2)::xs)
end (* local *)
 
fun reduceSelectIds env (at as SelTrans {selectids,guard,names}) =
let
val _ = Util.debugVeryDetailed (fn()=> ["* reduceSelectIds:before=\n",
toString [] at])
 
val senv = List.foldl (Env.addId Env.SelectScope) env selectids
fun clocksInExpr expr = not (Env.containsClocks senv expr)
 
fun f (s as (id, ty), (sids, expr, names)) =
case E.shrinkScope ((id, ty, false), clocksInExpr) expr of
NONE => (s::sids, expr, names)
| SOME reboundExpr => (sids, reboundExpr, names <\ id)
 
val (selectids', guard', names') = foldl f ([], guard, names)
(rev selectids)
(* reverse the selectids to handle masking of identical names,
* folding f has the effect of reversing them back. *)
 
val at' = SelTrans {selectids=selectids', guard=guard', names=names'}
val _ = Util.debugVeryDetailed
(fn()=> ["* reduceSelectIds:after =\n", toString [] at'])
in at' end
 
end
end
 
seltrans.sml
Property changes : Added: svn:keywords + Id
/sources.ml
4,6 ⟶ 4,8
*)
use "maketest/action_trans.sig";
use "maketest/actiontrans.sml";
use "maketest/sel_trans.sig";
use "maketest/sel_trans.sml";
use "maketest/clock_expression.sig";
use "maketest/clockexpression.sml";
use "maketest/clk_expr_trans.sig";
/sources.mlb
11,6 ⟶ 11,8
ann "nonexhaustiveMatch ignore" in
action_trans.sig
actiontrans.sml
sel_trans.sig
sel_trans.sml
clock_expression.sig
clockexpression.sml
clk_expr_trans.sig
/clk_expr_trans.sig
27,6 ⟶ 27,12
val fromATrans : Environment.env -> ActionTrans.t -> t
(* may raise ClockExpression.NonClockTerm *)
 
val fromSTrans : Environment.env
-> (symbol * Expression.ty) list
-> SelTrans.t
-> t
(* may raise ClockExpression.NonClockTerm *)
 
val toTrans : t -> {selectids: Expression.boundid list,
actionsubs: Expression.expr list,
guard: Expression.expr}
/transitionflipper.sml
46,6 ⟶ 46,7
and Env = Environment
and ECVT = ExpressionCvt
and ATrans = ActionTrans
and STrans = SelTrans
and ClkE = ClockExpression
and CETrans = ClkExprTrans
in struct
105,8 ⟶ 106,10
end
handle ClkE.NonClockTerm => raise FlipFailed "bad clock terms in invariant"
 
fun negateTransitions env (subtypes, trans : t list, invariant) = let
val _ = Util.debugIndent (Settings.Outline,fn()=>["=negateTransitions="])
(* 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. *)
177,6 ⟶ 180,55
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 cetran = CETrans.fromSTrans env subIdx (STrans.mergeTrans strans)
 
(* 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)
/maketest.sml
5,6 ⟶ 5,24
* Shift generic functions into xml/nta parse/parsed-nta.
*)
 
(* Regarding channel arrays:
* Currently the original partitioning technique is still avaiable.
* If the updated sweep binding technique proves to be better in all cases then
* the original could be removed, to simplify the code, by removing:
* * TF.negatePartitionedTrans
* * ClkTrans.t no longer needs actselect, as the action field provides
* the same information.
* the partition field can also be removed.
* * ClkTrans.t change the action field to a list of symbols and types
* (removing the dependency on ActionTrans).
* and thus simplify the rest of the module.
* (take all the SelectSub cases).
* * remove ClkTrans.fromATrans
* * partitions.sml
* * action_trans.sig, actiontrans.sml
* (replaced by sel_trans.sig, seltrans.sml)
*)
 
local structure P = ParsedNta
and E = UppaalParse.Expression
and ECvt = UppaalParse.ExpressionCvt
/clkexprtrans.sml
10,6 ⟶ 10,7
structure E = Expression
and ClkE = ClockExpression
and AT = ActionTrans
and ST = SelTrans
and Env = Environment
and ECVT = ExpressionCvt
in struct
112,6 ⟶ 113,23
names=used}
end
 
fun fromSTrans preenv actsels (ST.SelTrans {selectids, guard, names}) =
let
val senv = List.foldl (Env.addId Env.SelectScope) preenv selectids
val (guard, forall, used) = ClkE.fromExpr (names, senv, guard)
(* Note: ClkE.fromExpr ensures:
* intersection(selectids, forall) = emptyset
* as names includes selectids.
*)
in
CETrans {actselect=actsels,
gselect=selectids,
forall=forall,
partition=E.trueExpr,
guard=guard,
action=map (fn (nm, _)=>AT.SelectSub nm) actsels,
names=used}
end
 
local (**)
fun toBoundId (s, ty) = E.BoundId (s, ty)
/sel_trans.sig
New file
0,0 ⟶ 1,103
(* $Id$ *)
 
signature SEL_TRANS = sig
 
type expr = Expression.expr
and ty = Expression.ty
and symbol = Atom.atom
and symbolset = AtomSet.set
 
exception NonSimpleSelectIndex of expr
exception BadChannelIndex of {id: symbol, badty: ty, goodty: ty}
exception BadSubscriptCount
 
datatype t = SelTrans of {selectids: (symbol * ty) list,
guard: expr,
names: symbolset}
 
val makeIndexNames : int
-> {selectids: Expression.boundid list,
actionsubs: Expression.expr list,
guard: Expression.expr} list
-> symbol list
(* makeIndexNames n ts
* Return a list of n names for indexing a channel set. The new names will not
* conflict with any non-selectids used in the guards (i.e. state variables)
* Prefer names already used within the given list of transitions. *)
 
val fromTrans : (symbol * ty) list
-> {selectids: Expression.boundid list,
actionsubs: Expression.expr list,
guard: Expression.expr}
-> t
(* fromTrans asubs trans
* Transform trans into a SelTrans whose channel set is indexed by asubs.
*
* The names in asubs must not conflict with non-selectids in guard and
* actionsubs.
*
* First a mapping R is formed from:
* -first (needed to handle duplicates) selection bindings used
* in index to required bindings
* e.g. R(s) = s_0
* R(t) = s_2
* -required bindings to fresh names (to avoid capture)
* e.g. R(s_0) = s_0'
* R(s_1) = s_1'
* R(s_2) = s_2'
* Then it is used for simultaneous renaming in the selectids and guard.
*
* This involves processing each index expression.
* for a selectid i
* -if the type doesn't cover the whole dimension then && in a
* restriction clause (l <= s_i <= u) where i has the type int[l,u]
* -if used in an earlier index, s_j, then && the clause (s_i == s_j)
* -if doesn't match the current name then rename (s_i/i)
* and remove i from the list of selectids
*
* for a state expression e:
* -throw an exception if it contains selectids
* -&& the clause (si == R'(e)) to the guard
*)
 
val toTrans : (symbol * ty) list
-> t
-> {selectids: Expression.boundid list,
actionsubs: Expression.expr list,
guard: Expression.expr}
 
(* For the given set of transitions, ensure that all SelectSubs against the
* same array dimension have the same name. *)
 
val toString : (symbol * ty) list -> t -> string
 
val mergeTrans : t list -> t
(* Merge a list of transitions that have been created for a common channel set
* indexing list, taking care to avoid selection binding capture. *)
 
(* TODO: update *)
val reduceSelectIds : Environment.env -> t -> t
(* Assuming: update expressions are ignored
*
* Each select binding that:
* 1) is not used in a SelectSub
* 2) is not involved in a sub-expression containing clocks
* is turned into an exists binding.
*
* Condition (1) and the assumption mean that the scope of the binding is only
* important inside the guard expression.
*
* Condition (2) ensures that the new guard expression does not split clock
* zones.
*
* Doing this allows maketest to negate transitions that might otherwise fail
* with a select/forall conflict, such as:
* {selectids: (i : int[0,N - 1])
* actionsubs:
* guard: get_status(i)==APPR &&
* (forall (j : int[0,N - 1])
* j!=i && get_status(j)!=AWAY imply status[j][i]<M
* )
*)
end
 
sel_trans.sig
Property changes : Added: svn:keywords + Id