testclass ExitState for statechart ExitState {
	
	/* An exit through an unnamed exit point must be taken by the transition without exit point spec (it must also be unguarded). */
	@Test
	operation defaultExit(){ 
		enter
		assert active(ExitState.r.A)
		
		raise e
		proceed 1 cycle
		assert active(ExitState.r.E) 
	} 

	/* An exit through an named exit point must be taken by the transition with the matching exit point spec if it exists. */
	@Test
	operation namedExitThroughNamedTransition(){ 
		enter
		assert active(ExitState.r.A)
		
		raise f
		proceed 1 cycle
		assert active(ExitState.r.F) 
	} 

	/* An exit through an named exit point must be taken by the default transition if no transition for this exit point exists.  */
	@Test
	operation namedExitThroughDefaultTransition(){ 
		enter
		assert active(ExitState.r.A)
		
		raise g
		proceed 1 cycle
		assert active(ExitState.r.E) 
	} 


	/* If no event is raised then the statechart must remain in state A.  */
	@Test
	operation remainInA(){ 
		enter
		assert active(ExitState.r.A)
		
		proceed 1 cycle
		assert active(ExitState.r.A) 
	} 

}