The animator may also be driven through an ANIMATE Script (in Interactive, Execute Step or Execute Auto mode); the Scripts may be automatically created from an interactive session (so that they may be replayed against changed AMN) or may be edited from a template form. For both Execute modes, assertions on the output of operations, and on the state variables may be included in a Script and these are evaluated and displayed during execution.
The output of all three modes of driving the animator may be saved - in interactive mode through the Utilities Menu and in either executable mode through a dialog which appears at the end of the execution. An output file is saved as fifi.identifier.out and may subsequently be viewed through the Browse Output File option of the Animator Menu.
Animation (anm) is invoked from the Main
Environment for all currently analysed
specifications, and so all library
and generated machines
may be animated (a good way to familiarize oneself with their functionality!).
In this description, fifi is assumed to be the name of the
machine being animated.
Interactive, Execute Step and Execute Auto offer three different ways of driving the Animator.
Edit ANIMATE Script provides a way of editing an ANIMATE
Scrip ; an existing script may be edited or a new one be created (with
template optionally provided from an existing Script); dialog menus are
automatically provided).
Browse Output File provides a menu of previously saved State
Output files (created from the Utilities
Menu) which may be selected for browsing.
Clean Animator Files provides a menu of Script ( .anm ) and State Output files ( .out ) which may be removed when no longer needed. This option is also avaiable from the Utilities Menu.
No file "SRC/fifi.mch.thy" - creating templateindicating that no user-supplied theory is provided to supplement the Animator's library of re-write rules, but that a template theory file has been created in the SRC directory (see Providing More Rewrite Rules below); when theory is supplied, the display will read
"SRC/fifi.mch.thy" loadedprovided the theory files parses, and
"SRC/fifi.mch.thy" does not parse - not loadedotherwise, together with information showing the cause of the error.
Initialize state from ANIMATE Script?If you reply `No', the state of the machine will be initialized according to its specification. You will be asked to instantiate any machine parameters (which must be natural numbers or enumerated sets). The Animator will then calculate the instantiated machine constraints and present them in a simplified form. If the machine (or any of its subordinates) contains sets or constants a dialog will be presented so that they may be set, and, one set they will be represented in a simplified form.
It is recommended that all abstract sets are instantiated, otherwise realistic animation is usually not possible.
A `Yes' answer provides a menu from which the Script may be selected;
subsequent selection overrides the initialization given in the Abstract
Machine specification, and instead initializes the state of the Machine
to that saved on file; with machine parameters and context also being set.
The initial state is then displayed in the state window.
See figureOn selection of an operation, its specification is displayed together with its stated precondition. If the operation has input parameters, you will be asked to instantiate them, and the simplified precondition will be displayed:
You will also be asked to resolve any nondeterminacy (e.g. in an ANY guard). The Animator simplifies, as far as it can, the precondition (or guards) of an operation according to the current state of the Machine. Whatever the value of the precondition or guard, the specified state change is performed, with the value of any output and the final state reported in the state window:
The `Undo' option allows you to return to the state prior to the action of the last operation.
Animator Utilities provides another menu of operations.
Display Invariant/Don't Display Invariant provides a toggle to display the current state of the INVARIANT of the machine:
The `Quit' option allows you to leave the animation.
See figure
Edit theory file provides a means of adding rules to aid the animator simplification mechanism.
Restore initial state enables the animation to be restarted with the initial state.
Restart animation causes the animation to be restarted form scratch.
Set state variables enables the current values of the state variables to be overwritten.
Save output results in a prompt for a filename identifier, with the current output being recorded on that file ( SRC/fifi.identifier.out ); it is subsequently possiblt to browse output through the main Animator Menu.
Save as ANIMATE Script Initialisation enables an interactive animator session to be written to an ANIMATE Script in such a way that it may be used to initialise (machine parameters, state variables and context) an Interactive Animator session - a menu of such Scripts is automatically provided at the start of each interactive session.
Save as ANIMATE Script Executable enables an interactive animator session to be written to an ANIMATE Script and subsequently replayed either in Step or Auto mode (although it may be used in Interactive mode - see NOTE).
Clean Animator Files provides a menu of ANIMATE Script ( .anm ) and State Output files ( .out ) which may be removed when no longer needed. This option is also avaiable from the main Animator Menu.
ANIMATE machinename.identifier.anm [| PARAMETER_VALUES ? | value [| ; value |] SETS_VALUES ? | value [| ; value |] CONSTANTS_VALUES ? | value [| ; value |] ENUM_SETS_VALUES ? | value [| ; value |] |] OPERATIONS ini_operation [| ; operation |] END value ::= identifier = expression
ini_operation ::= INI_op [| : command_list |] | _set_state_variables : ( eql_list )
INI_op ::= INI_fifi
operation ::= ANM_op [| : command_list |] | { predicate }
AMN_op ::= [| varlist <-- |] identifier [| ( varlist ) |]
command_list ::= command [| , command |]command ::= local_vars ( eql_list ) | branch ( num )
eql_list ::= equality [| , equality |]
equality ::= identifier = value
Note that each of the clauses is optional (but see NOTE),
and that a clause containing ? is equivalent to the clause being
absent.
NOTE
A new Script may be created through the Edit ANIMATE Script option of the Animator Menu when a sub-menu will be provided offering the edit of an existing Script or the creation of a new one.
A template for a new Script may be achieved in one of two ways:
ANIMATE
Person3.demo.anm
PARAMETER_VALUES
max_person = 100
SETS_VALUES
SCALAR = 0..2147483646;
STRING = STRING;
PERSON = {p1 , p2 , p3 , p4 , p5}
CONSTANTS_VALUES
?
ENUM_SETS_VALUES
BOOL = {FALSE , TRUE};
CHAR = {B_SOH , B_STX , B_ETX , B_EOT , B_ENQ , B_ACK , B_BEL , B_BS , B_HT , B_LF , B_VT , B_FF , B_CR , B_SO , B_SI , B_DLE , B_DC1 , B_DC2 , B_DC3 , B_DC4 , B_NAK , B_SYN , B_ETB , B_CAN , B_EM , B_SUB , B_ESC , B_FS , B_GS , B_RS , B_US , B_SPACE , B_EXCL , B_QUOT , B_HSH , B_DOLL , B_PCT , B_AMP , B_SQUOT , B_OPAR , B_CPAR , B_MUL , B_PLUS , B_COM , B_MINUS , B_DOT , B_DIV , '0' , '1' , '2' , '3' , '4' , '5' , '6' , '7' , '8' , '9' , B_COL , B_SCOL , B_LESS , B_EQL , B_GTR , B_QUERY , B_CADD , 'A' , 'B' , 'C' , 'D' , 'E' , 'F' , 'G' , 'H' , 'I' , 'J' , 'K' , 'L' , 'M' , 'N' , 'O' , 'P' , 'Q' , 'R' , 'S' , 'T' , 'U' , 'V' , 'W' , 'X' , 'Y' , 'Z' , B_OBRK , B_SLSH , B_CBRK , B_HAT , B_UNL , B_BSQ , 'a' , 'b' , 'c' , 'd' , 'e' , 'f' , 'g' , 'h' , 'i' , 'j' , 'k' , 'l' , 'm' , 'n' , 'o' , 'p' , 'q' , 'r' , 's' , 'u' , 'v' , 'w' , 'x' , 'y' , 'z' , B_OBRC , B_BAR , B_CBRC , B_TLD , B_DEL};
SEX = {female , male}
OPERATIONS
INI_Person3;
rep , new_person <-- Add_person(rupert,91,male) : ( branch(1); loc_vars( pers = p5 ) );
{ rep = TRUE };
{ new_person = p5 };
rep <-- Print_person_details(p5);
{ rep = TRUE };
rep <-- Remove_person(p5);
{ rep = TRUE }
END
Note that if choices/local variables are nested in the AMN, the commands following the : must sequentially reflect the route to be taken: so, for example:
op :
(
branch(3);
branch(2);
loc_vars( (var1 = 13), (var2 = 77) )
)
would ensure that var1 and var2 were set in:
op = CHOICE ... OR ... OR CHOICE ... OR ANY var1,var2 WHERE ... END OR ... END OR ... END
At the end of animation, the user is invited to optionally save the
output (as a .out file).
Additionally one of the following is reported after the execution is
complete:
THEORY UserLibX IS rewrite_rule [ ; rewrite_rule ] END [| DEFINITIONS rewrite_rule [ ; rewrite_rule ] INCLUSIONS incl_file [ , incl_file ] |]The optional DEFINITIONS clause allows macro definitions in the form of rewrite rules to be applied to the rules of UserLibX before use. If the theory file does not exist, it is created by the system with two default macros; a DEFINITIONS clause comprising `?' is equivalent to an empty clause.
The optional INCLUSIONS clause allows other animator theory files to be loaded (and, of course, the process is recursive). Each inclusion should be the name of an animator theory file enclosed in double quotes (for example "SRC/fifi.mch,thy"). An INCLUSIONS clause comprising `?' is equivalent to an empty clause.
The simplification rules of UserLibX should be expressed as B rewrite rules (see section on the B_Platform).
For example:
bident(x) => [l]^[x] == [l,x]will re-write the expression
[aa,bb,cc]^[dd]to
[aa,bb,cc,dd]
btest(n>1) => fac(n) == fac(n-1)*nwill re-write the expression
fac(7)to
fac(7-1)*7
© B-Core
(UK) Limited, Last updated: 22 Feb 2002