testclass HistoryWithoutInitialStep for statechart HistoryWithoutInitialStep {
	
	@Test
	operation enterThroughInitialEntry(){ 
		init()
		assert active(HistoryWithoutInitialStep.main_region.B.r1.C)
		
		raise next
		proceed 1 cycle
		assert active(HistoryWithoutInitialStep.main_region.B.r1.D)
	}
	
	@Test
	operation enterCThroughHistory(){
		init()
		assert active(HistoryWithoutInitialStep.main_region.B.r1.C)

		raise toA
		proceed 1 cycle
		assert active(HistoryWithoutInitialStep.main_region.A)
		
		raise toHistory
		proceed 1 cycle
		assert active(HistoryWithoutInitialStep.main_region.B.r1.C)
	}
		 
	@Test
	operation enterDThroughHistory(){
		init()
		raise next
		proceed 1 cycle
		assert active(HistoryWithoutInitialStep.main_region.B.r1.D)

		raise toA
		proceed 1 cycle
		assert active(HistoryWithoutInitialStep.main_region.A)
		
		raise toHistory
		proceed 1 cycle
		assert active(HistoryWithoutInitialStep.main_region.B.r1.D)
	}
		
	operation init(){
		enter
		assert active(HistoryWithoutInitialStep.main_region.A) 
		
		raise toB
		proceed 1 cycle
	}
}