id	summary	reporter	owner	description	type	status	priority	milestone	component	version	resolution	keywords	cc
148	ClassCastException in dynamic package	zirkel	ywei	"When running the Laplace example as follows:

{{{
tass verify -simplify -reduce=urgent -deadlock=ignore examples/laplace/laplaceImpl_2_2.mmp -np 3
}}}

A ClassCastException is generated:

{{{
java.lang.ClassCastException: edu.udel.cis.vsl.minimp.dynamic.impl.type.ReferenceValueType cannot be cast to edu.udel.cis.vsl.minimp.dynamic.IF.type.ArrayValueTypeIF
	at edu.udel.cis.vsl.minimp.semantics.impl.Evaluator.variableReferenceValue(Evaluator.java:130)
	at edu.udel.cis.vsl.minimp.semantics.impl.Evaluator.referenceValue(Evaluator.java:222)
	at edu.udel.cis.vsl.minimp.semantics.impl.Evaluator.arrayElementReferenceValue(Evaluator.java:159)
	at edu.udel.cis.vsl.minimp.semantics.impl.Evaluator.referenceValue(Evaluator.java:225)
	at edu.udel.cis.vsl.minimp.semantics.impl.Executor.assignValue(Executor.java:244)
	at edu.udel.cis.vsl.minimp.semantics.impl.Executor.executeAssignment(Executor.java:251)
	at edu.udel.cis.vsl.minimp.semantics.impl.Executor.execute(Executor.java:102)
	at edu.udel.cis.vsl.minimp.verify.urgent.StateManager.nextStateSimple(StateManager.java:90)
	at edu.udel.cis.vsl.minimp.verify.urgent.StateManager.nextState(StateManager.java:77)
	at edu.udel.cis.vsl.minimp.verify.urgent.StateManager.nextState(StateManager.java:1)
	at edu.udel.cis.vsl.minimp.search.DfsSearcher.proceedToNewState(DfsSearcher.java:147)
	at edu.udel.cis.vsl.minimp.search.DfsSearcher.search(DfsSearcher.java:109)
	at edu.udel.cis.vsl.minimp.search.DfsSearcher.search(DfsSearcher.java:95)
	at edu.udel.cis.vsl.minimp.verify.Verification.verify(Verification.java:82)
	at edu.udel.cis.vsl.minimp.verify.Verification.verify(Verification.java:32)
	at edu.udel.cis.vsl.minimp.MiniMP.verify(MiniMP.java:415)
	at edu.udel.cis.vsl.minimp.MiniMP.main(MiniMP.java:483)

}}}"	defect	closed	major		front	1.0	fixed	dynamic, exception, laplace, type