The user may access the entire glossary, or click on any hilighted word in either the user manual or tutorial to obtain a definition.
Note: This manual assumes that StateClock is already installed on your
system. To get the StateClock software, click
here (5MB).
1. Alarm
and Pressure Module - introductory features.
2. Fischer
Mutual Exclusion
- classes.
3. Train
Gate
- use of temporal logic.
Introduction
Getting started
Creating a Project
Saving your work and
exiting StateClock
Loading a Project
Adding a module
Adding a sub module or a body
States and control variables
Clock and private variables
Interface
Events
Adding Comments
Classes
Mapping
Linking interface variables
Inheritance of interface
variables
Setting the Environment
Running a Simulation
Creating the Specification File
Generating the FTS file
Connecting to STeP
Appendix 1: Types
and variables
Appendix 2: Syntax of StateClock
Appendix3: Getting the StateClock application
StateClock is a tool for constructing systems consisting of reactive modules. This allows the user to model a real world problem by using StateClock and the rules of temporal logic. StateClock converts the user's model, consisting of reactive modules, into a fair transition system. The user also creates a specification file, which represents the requirements that user feels the model should meet. These files can be submitted to STeP and checked for correctness. Below is a representation of the a typical project in StateClock:
Here project is the ancestor of the two sub modules;
controller and plant.
Their respective reactive modules
are found in the bodies.
In general one should divide a problem into the controller, or machine,
and the plant, or application domain. Also it is usually better to reduce
the complexity of an individual module by creating a number of sub modules,
each modeling a portion of the more complex module.
Return to Contents.
Find yourself a workstation in the Ariel lab or, if connecting remotely, use the rlogin command and login to a workstation in the ariel lab. Do not run StateClock on the servers, as it is compute intensive.
(The Ariel and CAT labs have all the appropriate software already installed. See Getting the StateClock application if you do not have it installed on your workstation. You also need the STeP model-checker and theorem prover.)
At the prompt enter:
visual ~stateclock/StateClock/stateclock.im &
These windows should appear on your screen:
Press the Launch Application button to start StateClock. The following
window should appear:
This is the StateClock window. This is where you will create your
projects consisting of reactive modules.
Return to Contents.
The first step in creating a StateClock model of your real world problem is to create the project. There two ways you may do this.
1. Move your mouse arrow over the Project heading on the selection bar at the top of the StateClock window. Press the left mouse button and drag down to create, then release.
2. The preferred method is to place the mouse arrow in the small blank window under Project, then press the middle mouse button and hold it until the Add button appears and it becomes highlighted. Then release the button.
Whichever method you use the following window will appear:
Simply enter the name of your project, and press OK. The project's name
will appear in both the small project window and in the Modular Structure
window. Return to Contents.
There are two ways you can save your work.
1. In the StateClock window, choose File from the headings. Press the left mouse button and drop down menu appears with the options: Open, Save, Set path, and Exit. Open will look in your current directory for any files with the .stc extension. Save will create the .stc file with the name of your project with the stc extension applied to it. However you will not be able to save your project until you set the path, so that StateClock knows where to place your .stc file. Therefore when saving your first project, set the path from the root directory into your preferred directory.
2. The other way to save your work is to save the StateClock image itself. Under the Development, choose one of the two options: Save Image, or Save Image and Exit, to save the image. A word of warning: This file is at least 8Meg. Therefore you are probably better of saving the .stc file from the StateClock window.
When you have saved your work you should always exit StateClock by choosing
File from the window and selecting Exit. If you exit in other ways you
may leave the visualworks process still running after you have logged out.
Return to Contents.
Once you have saved your project with the .stc extension, you can load the project into StateClock with the following steps:
1. Make sure that you have set the path containg the .stc file.
2. Under File Access, select the Open option.
3. A window will appear that allows you to select the .stc file.
4. An outlined window will appear, simply left click the mouse to expose
the window.
5. Left click on the selected .stc file, and the bottom portion of the
.stc window will confirm you have selected a StateClock file.
6. If the file is larger than 50K, you will be asked whether to Get Contents
or Get Info. Get Contents displays the contents of the comment window associated
with the project, see Adding Comments. Get Info merely displays the time
of the last update to project.
7. Left click and hold the button over the Load option and the project
associated with the .stc file will be loaded into StateClock.
8. You must left click on Exit to close the file selection window.
Return to Contents.
Once a new project has been created, it must have a least one module. If you drag the mouse arrow over the project name in the Modular Structure window, the name should turn red. Now press and hold the middle mouse button, and you will see a pull down menu with the following selections:
Project
Module
Comment/Specification
Features
Here Project is actually two selections, Rename and Remove. Remove will
not erase the .stc file in your directory, only remove it from StateClock.
The Module selection allows only one selection, Create. If you move the
mouse button to Module, while holding the middle mouse button down, the
Create option becomes available. Just move the mouse over the create option,
and hold it there until the Create button is hilighted. Then you are asked
for the module's name. See below: module1
When have entered the name of the module, select OK and the module will
be displayed beneath the project as shown. You may add any number of modules
to the project. Return to Contents.
Once you have added a module to your project, you may either add a sub module to the module, or a body. Creating sub modules allows for simpler and more understandable models. The body of a module will contain the states and transitions associated with the module. Apart from instantiation from a class, see Classes, only the body contains states and transitions.
Adding a sub module to a module requires that you move the mouse over the module's name. It will be hilighted in red. Then hold down the middle mouse button and you will see a pull down menu with the following options:
Module
Sub module
Body
Environment
Comments/Specification
Features
Module has the options; Rename, Remove, Interface and Instantiate.
Remove will remove the module and all its sub modules
and their sub modules, etc.
Interface refers to all In, Out and Shared variables.
See Interface.
Instantiate allow you to inherit from a class. See Classes.
Sub module has a Create option. Selecting this option will cause a window
to appear asking you for the name of the sub module.
Body has a Create and a Remove option. If you select the Create option the following window will appear:
This window allows you to create the body of a module. In order to close
this window you must select Exit. Any changes made to the body will not
be lost by choosing Exit. The Body is composed of states, events, local
variables and interface variables. Each of these components is covered
in detail below. Return to Contents.
States represent a logical space where the flow of control resides. Either the control is in the default, or initial state, or it has come to rest in a given state because the events connecting it to the initial state have been taken and none of the events which lead away from this state have been taken. See Events for more details. There are two ways to create a state. One way is to select the Primitive Object from the main selection bar, and then to select Create from the pull down menu. The easier way is to place the mouse arrow over the main window, with the Module's name, and press the middle mouse button. The Add Primitive Object button will appear. Once this button becomes hilighted release the middle mouse button. Now, regardless of which method you chose, the following window will appear:
If you wish all of your states to be XOR, in which case the flow of control is serial, choose XOR. If you wish to create concurrent states, select AND. Which ever of the two you select the following window is displayed. Simply enter the name of the state and left click on accept.
If you selected XOR states then the following window is displayed.
StateClock requires a control variable for each module which has XOR states. A different value of this variable is assigned to each state, beginning at zero and incrementing by one, in the order you create the states. You may accept the default name provided by StateClock or enter your own.
If you have chosen XOR states, one state must act as the default, or initial,
state. If you have chosen AND states, then each end state must have internal
XOR states where one state, in each AND state, must act as the default,
or initial, state. StateClock assigns the first state you create to be
the default state, although you can override this by left clicking on the
state, to hilight it, and selecting Default under Primitive Object.
Once you select OK from the above window your state will appear as a small
rectangle. In the example below three states have been created.
This represents just a portion of the Body window. Here we have selected the StateClock default control variable. The value in brackets seen after the state name is the value of the control variable associated with that state. The default state is in bold. If you left click on an individual state it becomes hilighted. Then press the middle mouse button and the following options are available:
The zoom in option allows you to create XOR or AND states
within this state. If you choose this option you are presented with window
representing the internals of the state. Then you may select add primitive
object using the middle mouse key. As before you may choose XOR or
AND states. You may continue to nest states within states, however a good
rule of thumb is to avoid nesting to many levels. While it is possible
to construct a complicated project within a single body, your project will
be easier for you to understand and maintain if you use separate modules.
Separate modules allow for concurrent execution just as with AND states.
The add event feature allows you to create an event whose source
is the current state. If you chose this option, you must left click on
the destination state and give the event a name. Events allow you to control
the flow of execution. See Events.
The move option allows you to move the position of the state in the window. If you chose this option you are prompted to left click the mouse in the new position. Remember this does not operate as a click and drag feature.
The remove option is obvious as is rename.
The expose and resize options are used when you have nested states within states, and you wish to expose this property at the next level up. Resize allows you to expand the exposed state to view its entire contents. Once you have nested states within a parent state, the parent state will have a @ placed in the rectangle. In the example below, state2 was hilighted and the zoom in was chosen using the middle mouse button. Then two AND states where placed inside. Notice that the AND states have a dotted line perimeter. Normally AND states contain nested states.
Clock variables have their own data type specified by StateClock. The user is not required to supply its data type. Once you have entered the edit Body screen you can create a clock variable by simply pressing the middle mouse button over the clock window at the middle right of the screen. Once the Add button appears and is hilighted, you will be asked to enter the clock's name. Clock variable created in this manner is private and cannot be exported in the interface.
Clock variables are commonly known as user defined clocks. With each clock,
c, is associated an incremental value, C_c. If C_c = 0, then the clock
is stopped. If C_c = 1, then the clock is incrementing by one. If C_c =
-1, then the clock is counting down by one. StateClock allows you to control
the clock with a number of action commands that are used in events. In
the action, or function, portion of the event you may; start the clock
using start(c), stop the clock using stop(c), start counting up using cu(c),
start counting up from udv with cu(c(udv)), start counting down using cd(c),
start counting down from udv using cd(c(udv)). Also you may check if the
clock is ticking using ct(c). This would be used in the guard portion of
the event.
Other private variables are data variables. The top right window holds the data variables. Once again use your middle mouse button to declare a data variable and its data type. You may also define a new data type or a constant using the appropriate window in the Body screen.
See Types and Variables for a detail explanation of both Data and Clock variables.
A module's interface consists of its IN, OUT and SHARED variables. These variables allow the designer to logically connect different modules. A variable is a candidate to become an interface variable if it is already an interface variable with the parent, siblings or children of the module in question or it is created within the module. There are two basic ways to examine or edit the interface of a module. Firstly you can place your mouse button over the module's name and press the middle mouse button and select body, then select edit. Then within the body select interface. Or simply when pressing the middle mouse button over the module's name, select module interface. The interface window is shown below.
Candidate variables,
which we have already described, will be found in the Candidate Interface
Variable window. If you wish to make a candidate variable an actual interface
variable, left click on the candidate variable to hilight it, then left
click on the top select button. This will place the variable into the Actual
Interface Variable window. The module will only recognize actual interface
variables.
If you wish to create a new interface variable, move the mouse arrow over
the Actual Interface Variable window, and press the middle mouse button.
Then when Add is hilighted, release the mouse button. This will cause a
the following window to appear.
Here you have the option of creating a Data variable or a Clock variable. See Types and Variables for an explanation of both Data and Clock variables. If you chose Data, the you must also declare the data type. StateClock has three primitive data types; bool, string and int. After entering the name of your variable, terminate the name with a colon. Then enter a space and enter the primitive data type. (i.e. variable_name: bool) If you have created your own data type, then you may chose that type as a data type when declaring your data variable.
In the interface window you have the option of creating your own data type.
Once again use the middle mouse button in the Type window to Add a new
type to your interface. Below is an example of the type declaration window
with the new data type: module1_num = [0..2]. See Types and Variables,
appendix 1.
Also you may create a constant in your interface by once again pressing the middle mouse button over the Constant window. Your must declare your constant to have a single value. And the value must be either boolean, integer or string. If you chose a string value, it must be bounded with single quote marks.
If you wish to declare a clock variable, StateClock will display the following window.
You must enter only the clock name. StateClock knows that this is a clock variable. If you declare a clock variable as an interface variable, StateClock assumes that it is an OUT variable. StateClock automatically appends an * to every clock variable used as an interface variable in order to distinguish it from data variables.
If you left click on any of the actual interface variables, and then hold
down the middle mouse button you are presented with the following menu:
The Add option allows you to add another interface variable. Remove and
Rename are obvious. Detail provides information on the variable, such as
its initial value, its data type and its interface mode. Sort by allows
you to sort the interface variables by name or mode. Changes mode allows
you to change the interface mode to IN, OUT or SHARED. While a data variable
may have any of the three interface modes, clock variables can be either
IN or OUT but not SHARED.
It is also possible to make a control variable into an interface variable.
Simply left click on the control variable in the control variable window.
Then using the middle mouse button, you can chose to place it in the interface.
Control variables are always OUT interface variables. These can be very
useful as interface variables, because they indicate the state the module
is in at any given time.
Return to Contents.
Events in StateClock are
transitions between states in a module. The only way to move from one state
to another is via an event whose source is the initial state, and whose
destination is the final state. Events are unidirectional only. Events
may have the some source and destination state. Below is an illustration
of a typical module with a number of events. The way you create an event
is to left click on the source state, and hilight it. Then press and hold
the middle mouse button over this state. While still pressing the middle
mouse button, scroll down the menu to add event and release the mouse.
StateClock now prompts you to left click on the destination state. Once
you have done this, a small screen is displayed asking you to enter the
name of the event. As with the name of the states, try to use a short meaningful
name. Now StateClock draws an arrow from the source to the destination
state, with the event shown as a rectangle embedded in the arrow. Look
at the example below and the detailed description that follows.
This example is used only to illustrate the options available when creating
and using events. All events have the same structure. The name is followed
by the time bounds; lower and upper. These time bounds apply to the timer
associated with each event. The timer of each event begins counting up
from 0 as soon as the guard is true. If the timer is equal to the lower
bound, then the event can be taken. When the timer reaches the upper bound
the event becomes urgent. This disables the tick transition. The tick transition
is created by StateClock and represents the global clock. The timer advances
in step with the global clock. If at any time, before the event becomes
urgent, the guard becomes false, the event is disabled and the timer is
reset to 0.
The second line shows the guards of the event and the last line shows the
function, or action. The guard must be true for the event to be taken.
When the event is taken then the action is executed. The guard is composed
of boolean expressions using the connectives as described in Syntax of
StateClock, appendix 2.
In composing the action statement only the AND connective is used. Also
you may us the choose() function here. This is a StateClock convention
that allows StateClock to arbitrarily choose values for all of the listed
variables. This is useful when creating the .fts file for submission to
Step verification.
When you create an event you may edit the event by left clicking the event
to hilight it and using the middle mouse button. You will see the following
pull down menu.
Move allows you to move the event on the module window. Just left
click to the new position. Bounds allows you to edit the upper and lower
time bounds of the event. If you chose to make the event a fair transition,
then, as in event0, the time bounds are replaced by fair. This means that
the event must eventually be taken but we don't know when. Guard allows
you to edit the guard statement. Remember these are boolean expressions.
Function on the other hand is the action to be taken when the event is
taken. Here the data variables are assigned values. StateClock uses the
colon : to acts as an assignment. Other actions can be taken with clock
variables. See Clock variables.
Remove and rename are obvious. Hide will hide the guard and the function. When hidden you can chose expose to reveal them. Dest allows you to change the destination state. Shared allows you to share this event with another event in the same module. This means that both must be taken simultaneously. Therefore one shared event is likely to have to wait for the other event until both are taken. Detail will provide a detail window on the event.
In the above example, event0 is a fair transition. Its guard is begin
/\ ~stop and its function is to start the clock c1 counting down from 30.
Event1 has both lower and upper time bounds of 0. This implies that
as soon as the guard is true, event1 becomes urgent. Event2 is a self-loop
that increments stage once every tick. Event3 has an lower bound of 3 and
an upper bound of 6. if it had no guard it would always be enabled. (i.e.
its guard is true). In this case once stop is true its timer begins ticking.
Once its timer reaches 3 it is eligible to be taken, and if it becomes
5 it is urgent.
Return to Contents.
When you are building your project it is important to add comments to each module and the project itself. When someone else looks at your StateClock file the first thing they will do is to look at your comments. This should allow them to quickly understand the interface for each module and each module's purpose. It is wise to keep your comments concise and to the point.
You may add comments to a project or one of its modules by placing the
mouse arrow over the project name in the Modular Structure window and selecting
Comment/Specification using the middle mouse key. Then select Comment Edit.
This allows you to edit the comments associated with that module.
Return to Contents.
StateClock allows you create a class module and to create copies of this module within your project. Once you have instantiated a project module from a class module, you are allowed to change only the private variables, but you cannot change the interface of the module. Also you cannot change the class module once it has been instantiated within the project.Classes are very useful when you have a number of identical modules in a project however these classes are not like classes in OOP. You may not instantiate from two different classes. One class cannot inherit from another class.
You create a class by pressing the middle mouse button over the class window and holding it until the Create Class button is hilighted. You are then asked to name the class. Once you have entered a name you will see the name in the class window. Now left click on the name to hilight it, and press the middle mouse button and you will see the following menu.
Create class allows you to create another class. Remove and rename are obvious. Specification allows you to write a specification file for the class. See Creating the Specification File. Edit class is the choice if you wish to create the class module. Mapping allows you to change the value of the control variable associated with each state in a given module.
Select the Edit Class feature. You are presented with a screen very similar to the Body edit window. However to add a variable to the class interface, use the middle mouse button over the interface window. In most other ways building a class module is like building a Body module. Once you have added your states and events using appropriate private and interface variables, select Exit.
Once the class is created, it can be used to instantiate a module in the project. Simply create a module or a sub module and, using the middle mouse button, select under module the feature, instantiate. This will show the following window.
Now select the class to instantiate the module, by left clicking the
class. A check mark will appear beside the class. Then press the Do button.
Now an * will appear beside the module's name in the Modular Structure
window. Notice that instantiated modules do not have a Body. Their body
is inherited from the class.
Return to Contents.
Mapping allows you to re-assign the numerical value associated in each state in a module. In the modular structure window, highlight the module with middle mouse button pressed, and choose Mapping under Features, a mapping window shown below should pop up:
You can assign a number to the selected object in the Primitive Objects window by pressing middle mouse button within the Primitive Objects window. The Reset button restores the original values for each object. Auto arrange will assign each object in the Primitive Objects window a unique numberical value automatically. To take the changes into effect, press Apply & Close button.
The link feature allows two or more sibling modules to link interface variables to a single interface variable or a existing variable in the parent. The linking process could proceed up the ancestral path, linking interface variables of siblings at many levels. You can access the linking feature for a given module by pressing the middle mouse button over the module name, and selecting link from the feature option. The following window will be displayed.
In this case we have three modules; f1, f2 and f3. Each had a shared
variable, x, which were labeled f1_x, f2_x and f3_x by StateClock. Each
of these variables was chosen by holding the cntl key while left clicking
the variable names in the interface window. Then you may chose to link
these variables to a new name, which you enter in the Link to window, or
you may chose a variable from the parent's interface. Then press the Link
button and you are presented with a window asking you to select the variable
whose initial value will be used for the linked variable. You may chose
any of the variables being linked, but you need only chose one. Just left
click on the chosen variable and press OK.
Return to Contents.
Each module you create can inherit the interface variables of its parent,
its siblings and its children. These interface variables are called candidate
interface variables until you choose to place them in the actual interface
of the module using the interface feature. Until you place a candidate
interface variable in the actual interface you will not be able to use
that variable in your module as guards or functions of any event.
Return to Contents.
StateClock allows you to test each module separately. With each module having its own interface all IN and SHARED variables must have values generated by some external control. In a fully complete project, this would be another module, but to test each module separately, StateClock uses the environment. The environment is simply another module that initially contains a single state and one event. The event's function uses the choose() function to supply arbitrary vales to all the IN and SHARED interface variables of the module you wish to test. You access the environment for a given module by placing the mouse arrow over the module and pressing the middle mouse button. Select the environment feature, then choose either the default or edit option. Default is the default environment the StateClock supplies, whereas edit allows you to introduce new states and events to control the timing and values of the interface variables. Below is the default environment.
The default environment has a no fairness event, arbitrary_action, which
when taken chooses an arbitrary value for all IN and SHARED interface variables
for the module being tested. If you choose the edit option you have access
to all the OUT variables of the module and can use them in your guards.
Using the environment is very useful in testing your modules.
Return to Contents.
StateClock allows you to test your entire project or any module, including
its sub-tree, using a feature called simulation. If you test a module you
must create the appropriate environment, however when you test the entire
project an external environment is not necessary. To access the simulation
window, middle click mouse over the project or module. Hold the mouse down
until you get to features, then select simulation. The following window
will appear.
When selecting the module for a simulation, all children modules are listed. In this case we are simulating the entire project. If ran the simulation on only one module it would be necessary to set the environment. The default setting for this window is to choose all children. Simply choose Apply & Close. The next window to appear is the Composed Bodies window. This window shows you all the concurrent modules that are part of the simulation. Also appearing at the same time is the simulation window. Below is the simulation window for a large project.
The eligible events window contains all those events which are initially
available to be taken. The events which are urgent are in bold. When an
event is urgent, the tick event is disabled and therefore is not available.
It is important to remember this. If you wish the tick event to be compassionate
do not create a cycle of urgent transitions, or the tick event will never
be available.
You choose an event by left clicking to hilight the event, and then holding
down the middle mouse button until the execute button is pressed. This
will place the chosen event in the History list. As you choose events the
history list acts as a log of your program control flow. At any time you
may press the middle mouse button over the history window and you can save
the history of your simulation as a .his file. Also it is possible to load
an old history file into a new simulation. This is a powerful feature that
allow you to test revisions to your project against an old history file.
Other features of the simulation window are available. You may undo a chosen
event by pressing the Undo button. You may play an entire simulation by
pressing the Play button. You can repeat a chosen event using the Redo
button and you can start the simulation over fro the beginning by pressing
the Reset button. Another important feature is allows you to place a chosen
variable from the Rest of the variables window in the selected variables
window. Also, doble click an event in the history list will cause a series
of undo operations upto the selected event. It is often important to know
the value of important variables during every stage of the simulation.
Just left click on the chosen variable, and while holding down the left
mouse button move the arrow over the selected variable window. Then release
the mouse button. The variable should now be visible in the new window.
Interested condition can be expressed in the window Interested condition
as predicate, the status of the condition in the current state is shown
in the Status field. In addition, assign an integer x to the Advance
ticks field and press Run button will cause the simulator to execute tick
event x times.
The history of a simulation can tell you a great deal about the logical
structure of your modules. This is allows you to test your design in a
concrete manner. Also it provides you a tool that allows you to reveal
know problems in other peoples designs. However a simulation cannot prove
correctness. For correctness you must use a theorem solver like STEP.
Return to Contents.
A specification file can be produced for every module in your project including the project itself. A specification file consists of requirements written as boolean statements. These requirements are based on the correct behavior of the application domain. Normally the control variables of the application domain modules are used as arguments in the boolean statements. Also other statements are found in the specification file, such as sanity checks, used to verify the correctness of system assumptions that should be true for all modules or projects. Below is an example of a specification file written for sample project.
Each specification file must begin with SPEC. The % is used to start
a comment and statements that express the correct behavior of your project
or module must begin with PROPERTY. The characters appearing after PROPERTY
but before the : is the label assigned to the given property. Macros are
used to used make the properties more readable, especially for someone
not familiar with your project.
Return to Contents.
In order to prove the correctness of your project or module with respect
to the requirements found in your specification, it is necessary to convert
the StateClock model into a fair transition system. StateClock allows you
to convert your project, or any module into an fts file by simply choosing
the features option, which is available for each module or the entire project,
and selecting code generation. Simply hilight the module or project name
in the modular structure window and middle mouse click the name and select
code generation under feature. You will be prompted for a file name with
the fts extension. Now you are able to test your project for correctness
by submitting the specification file and the fts file to a theorem prover
such as STEP. Return to Contents.
STEP is a powerful tool which allows you to test the correctness of StateClock model. In this example we are using only the model checker feature of STEP, although STEP has a number of other useful features. Firstly, enter the following command line:
/cs/fac/src/step1.4a/bin/STeP &
This will bring up the following screen.
Select file from the available options and and then chose load transitions from the pull down menu. You will then see a screen that will show all files with the .fts extension in the current directory. If no files are visible choose the .fts feature to display them. Simply left click on the selected fts file in the left window.. See the example below.
Once you left click on the selected fts file STeP will create a module
system of your project or module. The module system will fully describe
your module or project by defining all variables, all transitions, or events,
and the way the events are related to each other.
Now you must load the specification file. Once again select under file
the load specification option. You will be presented with a window similar
to the last window shown. Now the files shown in the left hand window will
be those files with a .spec extension. Simply left click on the desired
file, and STep will load it. The first property in your spec file will
be displayed in STep as the goal. If you wish to select another property
as your goal select properties from the top menu bar and chose select goal.
Then chose the desired property.
Once the spec file is loaded you can attempt to prove that your fair transition
system satisfies the property shown by selecting modelcheck. You will see
the following window.
Simply select OK. STep will attempt ether find a counter example to
your assertion or prove that the assertion is correct. Once you select
OK, STep will prompt you with a request for a log file to hold the results
of its attempt to prove your assertion. The log file is important in determining
the source of any counter example that STep finds. The log file must have
an extension of .mclog. Simply chose your log file and STep will proceed
to attempt to prove your assertion.
When attempting to prove the correctness of large projects, STep will generate
a large number of states. It must look at every possible outcome. This
will lead to exponential explosion. You will find that STep will fail for
lack of space.
Return to Contents.
StateClock Types, Variables and Constants
A StateClock variable is either
a data variable, or a
a control variable, or
a clock variable of type CLOCK.
Data and clock variables can be declared in a module interface, or as
private body variables. Clock and Control variables may only appear in
the
interface with mode out.
Types
The basic types are bool, int, and string. The user can also declare an array of the basic types. New types can be defined as follows:
integer subtypes (declared by T1 = [3..9])
enumerated types (declared T2 = {'red', 'green',
'amber'})
a1: array [4..7] of int
a2: array [7..12] of T1
Note: It is best to avoid enumerated types for now, due to the fact
that STeP theorem prover will not accept two types with the same element,
e.g. T3
= {'blue', 'red"} will conflict with T2 above.
Data Variables
A data variable v can be one of the following types
a basic type
a boolean (declared
v: bool),
an integer variable
(declared v: int)
a string type (declared
v: string)
a new type (e.g. v: T1)
an array of basic or new types (e.g v: array [3..9]
of int)
Clock variables
A clock variable always has type CLOCK, where CLOCK is defined as type integer.
Associated with each clock variable c there is a corresponding clock increment variable denoted C_c.
When the clock is stopped:
C_c = 0.
When the clock is counting up:
C_c = +1.
When the clock is counting down: C_c = -1.
The C_c increment variable is not accessible in the action of a clockchart
event. However, in an event guard we may use the query ct(c) which is
defined by ct(c) == (C_c != 0). Thus ct(c) is true iff the clock is either
counting up or down.
A clock variable that is counting down, never goes lower than zero.
It is possible for a clock c to be at zero, and yet have ct(c) true. This
is because
ct(c) will only become false after a clock has been stopped.
Control Variables
The user does not create the type of control variables. Control variable
types are created automatically by StateClock. Each object name is mapped
to an integer value, and the type of the control variable is an integer
subtype. The control variable apm_pressure, for example, is declared by
StateClock to be: apm_pressure: [0..1].
Return to Contents.
In the current version of StateClock, variables can be declared as integer,
boolean, string, or user defined types. Declared variables can be used
in
guards and functions (actions).
A StateClock event such as E[l,u]: guard / function has a guard and
function (a set of actions). Assume that the following variables
have been
declared:
d1,d2: int
b: bool
c1,c2: CLOCK
Then a guard might look like:
((d1 > d2 +3), (d1 = 5), ct(c2)); (c1 =
20) ; ~(c2 = 1)
which stands for: ((d1 > d2 +3) /\ (d1 = 5)
/\ ct(c2)) \/ (c1 = 20) \/ ~(c2 = 1)
where ct(c2) == ~(C_c2 = 0), and where C_c2 is
the clock increment variable associated with clock c2.
A function might look like:
d1 := d1 + 1
d2 := d1
b := ~b
start clock c1 counting up
start clock c2 counting down from 25 time units.
| Operator | StateClock (Clockcharts) |
STeP spec Files |
| conjunction | , | /\ |
| disjunction | ; | \/ |
| negation | ~ | ~ or ! |
| equality | = | = |
| inequalities | <,<=,>,>= | <,<=,>,>= |
| integer operators | +,-,*,mod,div | +,-,*,mod,div |
| In update functions only | ||
| clock is ticking | ct(c) | C_c != 0 |
| start clock | start(c) | c = 0 /\ C_c != 0 |
| stop clock | stop(c) | C_c = 0 |
| start clock c counting up | cu(c) | |
| start clock c counting up from udv | cu(c(udv)) | |
| start clock c counting down | cd(c) | |
| start clock c counting down from udv | cd(c(udv)) | |
| set variables v1, v2 to arbitrary values | choose(v1,v2) | Declare "modvar v1,v2" in STeP transition file |
unzip stateclock.zip
visual StateClock.im
StartStateClock open
