The Symphony IDE

Formal Modelling for Systems of Systems

Go to our GitHub Profile

BitRegister_MC

Author: Jim Woodcock

This simple bit register example has been provided in VDM by a student called Andreas Mueller from Austria. It has been translated to CML by Jim Woodcock and used for testing the Symphony tool.

This example defines the main operators you can conduct on a very simple calculator where you can have registers you can store and load values to and from, and then add and subtract. The original version handles bytes up to 255. This cut-down version was produced by Adalberto Cajueiro to handle bytes up to 4 so it is possible to see the effect of overflows and underflows in the model checker.

The deadlock found by the model checker produced the same trace in the animator (except for the tau-events). A good exercise it to run these two plugins to observe the results.

The original version uses an input as the value to be incremented/decremented. This version uses a value that can be changed in each execution/analysis.

simpler-register.cml

--The original value for MAX is 255. Due to performance questions we use 4
--The value of increment establishes on how the reg variable is updated (incremented or decremented).
-- This can caus under or overflows.
values
MAX : nat = 4
increment : nat = 1

functions
oflow : int*int -> bool
oflow(i,j) == i+j > MAX

uflow : int*int -> bool
uflow(i,j) == i-j < 0

types
MYINT = nat
inv i == i in set {increment}

channels
init, overflow, underflow
inc, dec : MYINT

process RegisterProc =
begin

state
reg : int := 0

operations
INIT : () ==> ()
INIT() == reg := MAX - 1

ADD(i) == reg := reg + i

SUB: int ==> ()
SUB(i) == reg := reg - i

actions

REG =
(inc.increment -> [not oflow(reg,increment)] & ADD(increment);REG)
[]
(dec.increment -> [not uflow(reg,increment)] & SUB(increment);REG)
@
init -> INIT(); REG
end