Demo entry 6362081

Project2

   

Submitted by anonymous on May 07, 2017 at 04:51
Language: NuSMV. Code size: 3.4 kB.

MODULE main
VAR
	Gate :  gate(Controller.closegate);
	Train1 :  train(Controller.green1, Controller.approach1, Controller.leave1);
	Train2 :  train(Controller.green2, Controller.approach2, Controller.leave2);
	Controller :  controller(Gate, Train1, Train2);
	
JUSTICE TRUE;

--reachability
LTLSPEC F (Train1.state = crossing)
LTLSPEC F (Train2.state = crossing)
LTLSPEC F (Train1.state = crossing & Train2.state = crossing)

--safety
LTLSPEC G ((Train1.state = crossing | Train2.state = crossing) -> Gate.state = closed)
LTLSPEC G (Gate.state = open -> ! (Train1.state = crossing & Train2.state = crossing))

--liveness
LTLSPEC G (Train1.state = approaching -> F Train1.state = crossing)
LTLSPEC G (Train2.state = approaching -> F Train2.state = crossing)

MODULE controller(Gate, Train1, Train2)
VAR
	state : {outside, entering1, entering2, enteringBoth, inside1, inside2, insideBoth, leaving1, leaving2};
	green1 : boolean;
	green2 : boolean;
	approach1 : boolean;
	approach2 : boolean;
	leave1 : boolean;
	leave2 : boolean;
	closegate: boolean;
ASSIGN
	init(state) := outside;
	init(closegate) := FALSE;
	init(approach1) := FALSE;
	init(approach2) := FALSE;
	init(leave1) := FALSE;
	init(leave2) := FALSE;
	next(state) := case
		state = outside & approach1 : entering1;
		state = outside & approach2 : entering2;
		state = entering1 & approach2 : enteringBoth;
		state = entering2 & approach1 : enteringBoth;
		state = entering1 & Gate.state = closed : inside1;
		state = entering2 & Gate.state = closed : inside2;
		state = enteringBoth & Gate.state = closed : insideBoth;
		state = inside1 & approach2 : insideBoth;
		state = inside2 & approach1 : insideBoth;
		state = inside1 & leave1 : leaving1;
		state = inside2 & leave2 : leaving2;
		state = insideBoth & leave2 : inside1;
		state = insideBoth & leave1 : inside2;
		state = leaving1 & Gate.state = open : outside;
		state = leaving2 & Gate.state = open : outside;
		--these two below lines are the 'fixed' version
		state = leaving1 & approach2 : entering2;
		state = leaving2 & approach1 : entering1;
		TRUE : state;
	esac;
	
	next(closegate) := case
		state = entering1 & Train2.state = faraway | state = entering2 & Train1.state = faraway | state = enteringBoth: TRUE;
		state = leaving1 | state = leaving2 : FALSE;
		TRUE : closegate;
	esac;
	
	next(approach1) := Train1.state = faraway ? TRUE : FALSE;
	next(approach2) := Train2.state = faraway ? TRUE : FALSE;
	
	next(leave1) := Train1.state = crossing ? TRUE : FALSE;
	next(leave2) := Train2.state = crossing ? TRUE : FALSE;

	next(green1) := ((state = inside1) | (state = insideBoth)) ? TRUE : FALSE;
	next(green2) := ((state = inside2) | (state = insideBoth)) ? TRUE : FALSE;
	

MODULE gate(close)
VAR
	state : {open, closing, closed, opening};
ASSIGN
	init(state) := open;
	next(state) := case
		state = open & close : closing;
		state = closing : closed;
		state = closed & !close: opening;
		state = opening : open;
		TRUE: state;
	esac;

MODULE train(green, approach, leave)
VAR
	state : {faraway, approaching, stopped, starting, crossing};
ASSIGN
	init(state) := faraway;
	next(state) := case
		state = faraway & approach: approaching;
		state = approaching & green : crossing;
		state = approaching & !green : stopped;
		state = stopped & green : starting;
		state = stopped & !green : stopped;
		state = starting : crossing;
		state = crossing & leave: faraway;
		TRUE: state;
	esac;
	

This snippet took 0.01 seconds to highlight.

Back to the Entry List or Home.

Delete this entry (admin only).