crashing model

small.smv (text/plain), 1002 bytes, created by Panard on 2010-12-06 18:02:43 UTC

-- Model generated by BIOCHAM

MODULE main

VAR
R : 0..5;
a : boolean;
b : boolean;
c : boolean;
d : boolean;

ASSIGN
init(R) := 0;
next(R) := 1..5;

ASSIGN
init(a) :=FALSE;
next(a) := case
	R = 0 : TRUE;
-- R1.
	R = 1 : case
		(a) : {FALSE, TRUE};
		1 : a;
		esac;
-- R2.
	R = 2 : case
		(a) : {FALSE, TRUE};
		1 : a;
		esac;
-- R5.
	R = 5 : case
		(d) : TRUE;
		1 : a;
		esac;
	1 : a;
	esac;

ASSIGN
init(b) :=FALSE;
next(b) := case
	R = 0 : FALSE;
-- R1.
	R = 1 : case
		(a) : TRUE;
		1 : b;
		esac;
-- R3.
	R = 3 : case
		(b) : {FALSE, TRUE};
		1 : b;
		esac;
	1 : b;
	esac;

ASSIGN
init(c) :=FALSE;
next(c) := case
	R = 0 : FALSE;
-- R2.
	R = 2 : case
		(a) : TRUE;
		1 : c;
		esac;
-- R4.
	R = 4 : case
		(c) : {FALSE, TRUE};
		1 : c;
		esac;
	1 : c;
	esac;

ASSIGN
init(d) :=FALSE;
next(d) := case
	R = 0 : FALSE;
-- R3.
	R = 3 : case
		(b) : TRUE;
		1 : d;
		esac;
-- R4.
	R = 4 : case
		(c) : TRUE;
		1 : d;
		esac;
-- R5.
	R = 5 : case
		(d) : {FALSE, TRUE};
		1 : d;
		esac;
	1 : d;
	esac;