(* $Id: action_trans.sig 29 2008-03-30 04:30:23Z tbourke $ *)
|
(* $Id: action_trans.sig 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.
|
|
*)
|
|
|
signature ACTION_TRANS = sig
|
signature ACTION_TRANS = sig
|
|
|
type expr = Expression.expr
|
type expr = Expression.expr
|
and ty = Expression.ty
|
and ty = Expression.ty
|
and boundid = Expression.boundid
|
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 MixedSubscriptTypes of expr * expr
|
exception ActSubWithNonSimpleSelect of expr
|
exception ActSubWithNonSimpleSelect of expr
|
exception ActSubWithBadType of {expr: expr, badty: ty, goodty: ty}
|
exception ActSubWithBadType of {expr: expr, badty: ty, goodty: ty}
|
exception BadSubscriptCount
|
exception BadSubscriptCount
|
|
|
(* transition actions have been checked against restrictions *)
|
(* transition actions have been checked against restrictions *)
|
datatype actionsub = SelectSub of symbol | FreeExprSub of expr
|
datatype actionsub = SelectSub of symbol | FreeExprSub of expr
|
datatype t = ActTrans of {selectids: (symbol * ty) list,
|
datatype t = ActTrans of {selectids: (symbol * ty) list,
|
actionsubs: actionsub list,
|
actionsubs: actionsub list,
|
guard: expr,
|
guard: expr,
|
names: symbolset}
|
names: symbolset}
|
|
|
val addSelectSubNames : actionsub list -> symbolset
|
val addSelectSubNames : actionsub list -> symbolset
|
val addFreeExprNames : actionsub list -> symbolset
|
val addFreeExprNames : actionsub list -> symbolset
|
val addActionNames : actionsub list -> symbolset
|
val addActionNames : actionsub list -> symbolset
|
val actionsubToExpr : actionsub -> expr
|
val actionsubToExpr : actionsub -> expr
|
|
|
val fromTrans : ty list -> {selectids: Expression.boundid list,
|
val fromTrans : ty list -> {selectids: Expression.boundid list,
|
actionsubs: Expression.expr list,
|
actionsubs: Expression.expr list,
|
guard: Expression.expr} -> t
|
guard: Expression.expr} -> t
|
(* Transform the given transition by categorising each action subscript as
|
(* Transform the given transition by categorising each action subscript as
|
either:
|
either:
|
* a SelectSub (index is single select identifier),
|
* a SelectSub (index is single select identifier),
|
* or a FreeExprSub (index expression contains no select identifiers).
|
* or a FreeExprSub (index expression contains no select identifiers).
|
Ensuring that SelectSub identifiers select from the entire subscript range
|
Ensuring that SelectSub identifiers select from the entire subscript range
|
(i.e. their type matches the corresponding array index type.)
|
(i.e. their type matches the corresponding array index type.)
|
|
|
TODO: comments about renaming select ids
|
TODO: comments about renaming select ids
|
*)
|
*)
|
val toTrans : t -> {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}
|
|
|
val ensureConsistency : t list -> t list
|
val ensureConsistency : t list -> t list
|
(* If two transitions refer to the same action then group them together.
|
(* If two transitions refer to the same action then group them together.
|
|
|
Ensure that action subscripts in the same dimension have the same
|
Ensure that action subscripts in the same dimension have the same
|
category (both are either a FreeExprSub or both are a SelectSub).
|
category (both are either a FreeExprSub or both are a SelectSub).
|
Ensure that SelectSub subscripts in the same dimension have the same name
|
Ensure that SelectSub subscripts in the same dimension have the same name
|
(i.e. call renameSelectIds first)
|
(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 coverMissingChannels : ty list * t list * Expression.expr -> t list
|
(* TODO: comments
|
(* TODO: comments
|
* the last expr is the location invariant. *)
|
* the last expr is the location invariant. *)
|
|
|
val toString : t -> string
|
val toString : t -> string
|
|
|
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
|
* 2) is not involved in a sub-expression containing clocks
|
* 2) is not involved in a sub-expression containing clocks
|
* is turned into an exists binding.
|
* is turned into an exists binding.
|
*
|
*
|
* Condition (1) and the assumption mean that the scope of the binding is only
|
* Condition (1) and the assumption mean that the scope of the binding is only
|
* important inside the guard expression.
|
* important inside the guard expression.
|
*
|
*
|
* Condition (2) ensures that the new guard expression does not split clock
|
* Condition (2) ensures that the new guard expression does not split clock
|
* zones.
|
* zones.
|
*
|
*
|
* Doing this allows maketest to negate transitions that might otherwise fail
|
* Doing this allows maketest to negate transitions that might otherwise fail
|
* with a select/forall conflict, such as:
|
* with a select/forall conflict, such as:
|
* {selectids: (i : int[0,N - 1])
|
* {selectids: (i : int[0,N - 1])
|
* actionsubs:
|
* actionsubs:
|
* guard: get_status(i)==APPR &&
|
* guard: get_status(i)==APPR &&
|
* (forall (j : int[0,N - 1])
|
* (forall (j : int[0,N - 1])
|
* j!=i && get_status(j)!=AWAY imply status[j][i]<M
|
* j!=i && get_status(j)!=AWAY imply status[j][i]<M
|
* )
|
* )
|
*)
|
*)
|
end
|
end
|
|
|
|
|