AToMPM/users/(default)/Formalisms/TrafficLight/Translational/traffic.mdepth

Model Traffic {
	Node State {
		name : String {id};
		red : boolean = false;
		green : boolean = false;
		yellow : boolean = false;
		timed : TimedTransition[0..1];
		interrupts : InterruptTransition[*];
	}

	Node InitialState[1] : State {
	}

	Node Transition {
		target : State;
	}

	Node TimedTransition : Transition {
		after : int;
	}

	Node InterruptTransition : Transition {
		interrupt : String;
	}

	Node Time[1] {
		clock : int = 0;
	}

	Node Interrupt {
		at : int;
		event : String;
		next : Interrupt[0..1];
	}
}

Traffic trafficLight {
	// standard routine
	InitialState red {
		name = "red";
		red = true;
		timed = toGreen;
		interrupts = [policeManOn, terminate];
}
State green {
	name = "green";
	green = true;
	timed = toYellow;
		interrupts = [policeManOn, terminate];
}
State yellow {
	name = "yellow";
	yellow = true;
	timed = toRed;
		interrupts = [policeManOn, terminate];
}
TimedTransition toGreen {
	after = 10000;
	target = green;
}
TimedTransition toYellow {
	after = 6000;
	target = yellow;
}
TimedTransition toRed {
	after = 2000;
	target = red;
}// blinking routine
State blinkOn {
	name = "blink";
	yellow = true;
	timed = toOff;
	interrupts = [lightsOn, terminate];
}
State blinkOff {
	name = "unblink";
	timed = toOn;
	interrupts = [lightsOn, terminate];
}
TimedTransition toOn {
	after = 1000;
	target = blinkOn;
}
TimedTransition toOff {
	after = 1000;
	target = blinkOff;
}

// transitions between routines
InterruptTransition policeManOn {
	interrupt = "Policeman";
	target = blinkOn;
}
InterruptTransition lightsOn {
	interrupt = "Light";
	target = red;
}

// terminate
State terminated {
	name = "STOP";
}
InterruptTransition terminate {
	interrupt = "stop";
	target = terminated;
}

// environment
Time t {
}
Interrupt i1 {
	at = 40000;
	event = "Policeman";
	next = i2;
}
Interrupt i2 {
	at = 	60000;
	event = "Light";
	next = i3;
}
Interrupt i3 {
	at = 90000;
	event = "stop";
}

}