id	summary	reporter	owner	description	type	status	priority	milestone	component	version	resolution	keywords	cc
75	Problems with tass verify, ArrayIndexOutOfBounds Exception	rdeaton	Stephen Siegel	"Run on latest svn, [1063]. Trace is attached.

MiniMP rdeaton$ ./tass verify examples/simpleMP/simpleMPImplGood.mmp 
+----------------------------------------------------------------------+
|           TASS: Toolkit for Accurate Scientific Software             |
|  version 1.0.r1054 (2009-08-29)        http://vsl.cis.udel.edu/tass  |
+----------------------------------------------------------------------+
                   command            : verify
                   model              : simpleMPImplGood.mmp(np=1)
                   Deadlock detection : absolute
                   Reduction          : standard
                   verbose:           : No
                   simplify:          : No
                   bufferBound        : 10
                   use loop technique : false

java.lang.ArrayIndexOutOfBoundsException: 1
	at edu.udel.cis.vsl.minimp.model.impl.Model.process(Model.java:526)
	at edu.udel.cis.vsl.minimp.semantics.impl.Evaluator.process(Evaluator.java:349)
	at edu.udel.cis.vsl.minimp.semantics.impl.Evaluator.evaluateNotEmpty(Evaluator.java:370)
	at edu.udel.cis.vsl.minimp.semantics.impl.Evaluator.evaluate(Evaluator.java:159)
	at edu.udel.cis.vsl.minimp.verify.std.Enabler.proceedToNext(Enabler.java:74)
	at edu.udel.cis.vsl.minimp.verify.std.Enabler.enabledTransitions(Enabler.java:105)
	at edu.udel.cis.vsl.minimp.verify.std.Enabler.enabledTransitions(Enabler.java:18)
	at edu.udel.cis.vsl.minimp.search.DfsSearcher.proceedToNewState(DfsSearcher.java:146)
	at edu.udel.cis.vsl.minimp.search.DfsSearcher.search(DfsSearcher.java:102)
	at edu.udel.cis.vsl.minimp.search.DfsSearcher.search(DfsSearcher.java:88)
	at edu.udel.cis.vsl.minimp.verify.Verification.verify(Verification.java:90)
	at edu.udel.cis.vsl.minimp.Minimp.verify(Minimp.java:441)
	at edu.udel.cis.vsl.minimp.Minimp.main(Minimp.java:535)
java.lang.ArrayIndexOutOfBoundsException: 1
No deadlock possible at this state.
Writing counterexample to simpleMPImplGood.trace...done.
Writing model to simpleMPImplGood.model...done.
Program terminated.
Property doesn't hold: counterexample found.
Execution time is: 0.298s.
"	defect	closed	major		semantics	1.0	fixed