| Line 1... |
Line 1... |
(* $Id: action_trans.sig 29 2008-03-30 04:30:23Z tbourke $ *)
|
(* $Id: sel_trans.sig 44 2008-05-10 11:23:01Z tbourke $ *)
|
|
|
signature ACTION_TRANS = sig
|
signature SEL_TRANS = sig
|
|
|
type expr = Expression.expr
|
type expr = Expression.expr
|
and ty = Expression.ty
|
and ty = Expression.ty
|
and boundid = Expression.boundid
|
|
and symbol = Atom.atom
|
and symbol = Atom.atom
|
and symbolset = AtomSet.set
|
and symbolset = AtomSet.set
|
|
|
exception MixedSubscriptTypes of expr * expr
|
exception NonSimpleSelectIndex of expr
|
exception ActSubWithNonSimpleSelect of expr
|
exception BadChannelIndex of {id: symbol, badty: ty, goodty: ty}
|
exception ActSubWithBadType of {expr: expr, badty: ty, goodty: ty}
|
|
exception BadSubscriptCount
|
exception BadSubscriptCount
|
|
|
(* transition actions have been checked against restrictions *)
|
datatype t = SelTrans of {selectids: (symbol * ty) list,
|
datatype actionsub = SelectSub of symbol | FreeExprSub of expr
|
|
datatype t = ActTrans of {selectids: (symbol * ty) list,
|
|
actionsubs: actionsub list,
|
|
guard: expr,
|
guard: expr,
|
names: symbolset}
|
names: symbolset}
|
|
|
val addSelectSubNames : actionsub list -> symbolset
|
val makeIndexNames : int
|
val addFreeExprNames : actionsub list -> symbolset
|
-> {selectids: Expression.boundid list,
|
val addActionNames : actionsub list -> symbolset
|
|
val actionsubToExpr : actionsub -> expr
|
|
|
|
val fromTrans : ty list -> {selectids: Expression.boundid list,
|
|
actionsubs: Expression.expr list,
|
actionsubs: Expression.expr list,
|
guard: Expression.expr} -> t
|
guard: Expression.expr} list
|
(* Transform the given transition by categorising each action subscript as
|
-> symbol list
|
either:
|
(* makeIndexNames n ts
|
* a SelectSub (index is single select identifier),
|
* Return a list of n names for indexing a channel set. The new names will not
|
* or a FreeExprSub (index expression contains no select identifiers).
|
* conflict with any non-selectids used in the guards (i.e. state variables)
|
Ensuring that SelectSub identifiers select from the entire subscript range
|
* Prefer names already used within the given list of transitions. *)
|
(i.e. their type matches the corresponding array index type.)
|
|
|
|
TODO: comments about renaming select ids
|
val fromTrans : (symbol * ty) list
|
*)
|
-> {selectids: Expression.boundid list,
|
val toTrans : t -> {selectids: Expression.boundid list,
|
|
actionsubs: Expression.expr list,
|
actionsubs: Expression.expr list,
|
guard: Expression.expr}
|
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 ensureConsistency : t list -> t list
|
val toTrans : (symbol * ty) list
|
(* If two transitions refer to the same action then group them together.
|
-> t
|
|
-> {selectids: Expression.boundid list,
|
|
actionsubs: Expression.expr list,
|
|
guard: Expression.expr}
|
|
|
Ensure that action subscripts in the same dimension have the same
|
|
category (both are either a FreeExprSub or both are a SelectSub).
|
|
Ensure that SelectSub subscripts in the same dimension have the same name
|
|
(i.e. call renameSelectIds first)
|
|
*)
|
|
(* For the given set of transitions, ensure that all SelectSubs against the
|
(* For the given set of transitions, ensure that all SelectSubs against the
|
* same array dimension have the same name. *)
|
* same array dimension have the same name. *)
|
|
|
val coverMissingChannels : ty list * t list * Expression.expr -> t list
|
val toString : (symbol * ty) list -> t -> string
|
(* TODO: comments
|
|
* the last expr is the location invariant. *)
|
|
|
|
val toString : 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
|
val reduceSelectIds : Environment.env -> t -> t
|
(* Assuming: update expressions are ignored
|
(* Assuming: update expressions are ignored
|
*
|
*
|
* Each select binding that:
|
* Each select binding that:
|
* 1) is not used in a SelectSub
|
* 1) is not used in a SelectSub
|
* 1) is not used in a SelectSub
|
* 1) is not used in a SelectSub
|