CSPM
Statements
Variable
and Signal Declarations
Process
Definitions
Program
Declarations
Assertions
Comments
If you just want to convert a source file into a CSPM script run 'java Parser SOURCE DEST'. In order to run it in FDR the destination directory should contain a copy of share2priorities.csp.
To launch the GUI run 'java InterpreterGUI'.
The GUI converts a source file into a CSPM script and can run FDR on it and interpret the results produced. The table in the top left contains a list of all the assertions made in the source file. When you select one, the result appears below and, if it was false, a counterexample is given in the table beneath. In order to simplify the traces, the checkboxes in the top right can be used to hide certain events if you are not interested in them.
On loading a file, you will not be able to view the traces until you have run FDR, using the button in the top right. Alternatively, if you have previously done this there are options in the file menu to load and save results.
Additionally command line options can be used with the form 'java InterpreterGUI source' followed by any of ' -r=ReadOutputFile -w=WriteOutputFile -c=CSPFile'. This will automatically load and run FDR for the source file specified. If the -c=CSPFile flag is used the resulting CSPM script is saved in CSPFile. The -w=WriteOutputFile is used to save the output from FDR. If -r=ReadOutputFile option is used then instead of running FDR it will try to interpret the results found in ReadOutputFile. If this last option is used then the other two flags are ignored.
It should be noted that unless these flags are used to specify otherwise, the GUI will create files (and overwrite any existing files) named “output.csp” and “results”.
A source file consists of some or all of the following things in any order:
If the compiler encounters %% then the rest of the line is copied as is into the output file. No checks are made on its content.
This mechanism should be used to define the constants:
atomic_exprs – denoting whether the evaluation of expressions should be executed atomically
sba and sia – the sizes of the boolean and integer arrays respectively
MinI and MaxI – the lower and upper bounds on the values integer variables and expressions can range over
InitI and InitB – the default initial values for integer and boolean variables respectively
Variable declarations follow the format
TYPE NAMES ;
where TYPE can be any of int, int[], bool, bool[] and NAMES is a comma seperated list of names. A name must consist entirely of numbers and letters, must start with a letter and must not clash with any of the reserved words.
Each name may optionally be followed by an initialisation of the form NAME = VALUE.
Arrays can be initialised by giving a comma separated list of values enclosed within < and >. The list must not be longer than the size of the corresponding array, although it can be shorter, in which case the final elements are assigned the default value for their type.
Global integer constants can be defined by
const NAMES ;
where NAMES is a list of names, all of which must be initialised as above.
Signals come in two sorts: signals which transmit an integer value and those which don't. These are declared by
isig NAMES
;
sig NAMES ;
The individual sequential processes are declared by
NAME ( ARGS ) = PROG
ARGS is a list of the names of the integer arguments this process takes. It can be empty.
PROG is either a single CMD or a semicolon separated list of CMDs enclosed within { }.
CMD is defined by
CMD ::= skip
| iter PROG
|
while BEXPR do PROG
| do PROG while
BEXPR
| if BEXPR then PROG
| if BEXPR then
PROG else PROG
| IVAR := IEXPR
| BVAR :=
BEXPR
| sig ( SIGNAME )
| isig ( ISIGNAME
, IEXPR )
| atomic PROG
| idle
BEXPR ::= ! BEXPR
| BEXPR &&
BEXPR
| BEXPR || BEXPR
| IEXPR = IEXP
| IEXPR
>= IEXPR
| IEXPR > IEXPR
| IEXPR >=
IEXPR
| IEXPR < IEXPR
| ( BEXPR )
|
true
| false
| BVAR
IEXPR ::= IEXPR + IEXPR
| IEXPR – IEXPR
| IEXPR *
IEXPR
| IEXPR / IEXPR
| IEXPR % IEXPR
| max
( IEXPR , IEXPR )
| min ( IEXPR ,
IEXPR )
| - IEXPR
| ( IEXPR )
|
CONST
| NUM
| IVAR
Here CONST matches either a global constant or the argument to a process, NUM matches an integer literal, SIGNAME,ISIGNAME,IVAR and BVAR match signals and variables of the appropriate type. Signals and variables must be declared before they are used. Arrays are accessed by expressions of the form NAME [ IEXPR ] but the indexing expression must be a compile time constant (i.e. cannot use any variables).
The meaning of most of the commands should be fairly clear, but there are a few that are less obvious. iter runs a piece of code over and over and so is equivalent to while true do. atomic executes a piece of code atomically. idle signals that a process with a lower priority should be allowed to perform one action and is discussed further in the program declarations section. sig and isig are used to output signals to the outside world.
Processes are combined together into “programs”. Even if you wish to perform checks about a single process it must still be declared as a program separately from its definition as a process. Programs as defined as follows:
NAME = < PROCESSES >
Where PROCESSES is a non-empty comma separated list of processes, with each process being passed its arguments using the syntax NAME ( ARGS ).
It is possible to declare a program to have a monitor process by instead declaring
NAME = < PROCESSES > with MONITOR watching { VARS }
VARS must be a list of variables. If you wish to monitor an array, each element must be listed individually. Every time an assignment is made to any of the variables listed in VARS the MONITOR process is run to completion before any other process is allowed to proceed. If such an assignment is made inside an atomic section the monitor waits for the atomic section to be completed before running.
It is also possible to declare that certain processes have a higher priority than others. In this case PROCESSES should instead be a list of lists of processes, each list surrounded by < >. The processes in any one list are given the same priority level but the lists themselves should be in decreasing order of priority.
A process in a lower level is only allowed to perform an action if all the processes in the level above synchronise on executing the idle command. An action is taken to be a single event in the underlying CSPM interpretation of the program. This means either a variable read/write, the start/end of an expression evaluation, a signal or an idle. However, the entirety of an atomic section is counted as a single action. Whenever the processes in a level synchronise on executing an idle command it only allows one of the processes in the level below to execute an action. The exception to this is when all the processes in that level themselves synchronise on an idle to allow a process in the level below that to perform some action. It should be noted that a process will not be blocked by waiting to synchronise on an idle command. If the other processes in its level are not ready to perform idles it can perform its idle and move on. This will have the effect of signalling “noop” and will not allow a process at a lower level to proceed.
Using priorities can require a huge number of steps to be taken at higher levels to produce an effect at the lower levels and so the traces produced by FDR become very long and it can take a long time to check them. Because of this it is generally advised to avoid using priorities if possible.
There are two kinds of assertion, boolean conditions and signal assertions. (others assertions can be made using %% but the trace interpreter will not interpret the results for you, as it cannot know which processes are involved).
Boolean conditions have the one of the forms:
assert always BEXPR in
PROGRAM
assert never BEXPR in PROGRAM
As you would expect these check whether the boolean expression given (presumably involving some variables) is caused to become false or true respectively by any execution path of PROGRAM.
Signal assertions have the form
assert nosignal { SIGNALS } in PROGRAM
This tests whether any of the signals given are ever output by PROGRAM. If you wish to test for one of the signals which can transmit an integer value, the value you wish to check for must be given by NAME.NUM, where number is an integer literal. The special signal outofrange can be tested for to check if any integer value goes out of the range declared by MinI and MaxI. Note that this is the only way this signal can occur. It cannot explicitly be outputted by using the sig command.
Comments can be added using //. Whenever // is encountered the rest of the line is ignored.
The GUI requires Java 1.6 and FDR2 - fdr2 must be in your PATH