ClassCastException in dynamic package

[zirkel]

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)

[Stephen Siegel]

The problem is in the model builder, which as not handled the select statement correctly. It had put the target location for the select statement in a completely different function (jacobi), which caused corruption of the state later on. I added code to the Model class to check that the target location is in the same function as the statement, so that now this example will throw a syntax exception during model building. Model builder needs to be fixed.

[Stephen Siegel]

Fixed by Yi earlier.