------------------------------------------
Fichier de sortie Promela : clapet.promela
------------------------------------------

#define TRUE  1
#define FALSE 0

mtype = { ouvert, ferme };
int temp;
mtype clapet;

never {
	do
	::assert((temp <= 30) && (clapet == ferme))
	od
}

proctype init_sys() {
	temp = 20;
	clapet = ferme;
}

proctype fermerClapet () {
	clapet = ferme;
}

proctype ouvrirClapet () {
	clapet = ouvert;
}

proctype monterTemp () {
	if
	::temp = (temp+1);
	::temp = (temp+3);
	fi
}

proctype baisserTemp () {
	assert((temp > 10))
	temp = temp-1;
}

init {
	run init_sys();
}