id	summary	reporter	owner	description	type	status	priority	milestone	component	version	resolution	keywords	cc
142	Class cast exception in diffusion1	Stephen Siegel	ywei	"There is a class cast exception in the symbolic package.
This time I have checked in the two mmp source files: they have the string ""_CAST"" in their filenames.  If you run them with the options shown below, you will get the exception:

{{{
+----------------------------------------------------------------------+
|           TASS: Toolkit for Accurate Scientific Software             |
|  version 1.0.r1240 (2009-12-20)        http://vsl.cis.udel.edu/tass  |
+----------------------------------------------------------------------+
       specification : diffusion_seq (numProcs = 1)
      specSourceFile : examples/diffusion/diffusion_seq.mmp
      implementation : diffusion1_par (numProcs = 2)
      implSourceFile : examples/diffusion/diffusion1_par.mmp
                mode : COMPARE
              prover : CVC3
            deadlock : IGNORE
           reduction : URGENT
            simplify : false
             verbose : false
         loop method : false
          repository : ./TASSREP

Comparing diffusion_seq and diffusion1_par...

java.lang.ClassCastException: edu.udel.cis.vsl.minimp.symbolic.expression.SymWriteExpression cannot be cast to edu.udel.cis.vsl.minimp.symbolic.expression.SymConstant
	at edu.udel.cis.vsl.minimp.symbolic.expression.SymConstant.compareToLocal(SymConstant.java:74)
	at edu.udel.cis.vsl.minimp.symbolic.expression.SymWriteExpression.compareToLocal(SymWriteExpression.java:88)
	at edu.udel.cis.vsl.minimp.symbolic.expression.SymWriteExpression.compareToLocal(SymWriteExpression.java:88)
	at edu.udel.cis.vsl.minimp.symbolic.SymUniverse.compare(SymUniverse.java:1414)
	at edu.udel.cis.vsl.minimp.symbolic.SymUniverse.equalsExpression(SymUniverse.java:1103)
	at edu.udel.cis.vsl.minimp.dynamic.impl.DynamicFactory.equalsSymbolic(DynamicFactory.java:348)
	at edu.udel.cis.vsl.minimp.dynamic.impl.DynamicFactory.equals(DynamicFactory.java:340)
	at edu.udel.cis.vsl.minimp.verify.IF.InnerPredicate.holdsAt(InnerPredicate.java:122)
	at edu.udel.cis.vsl.minimp.verify.IF.InnerPredicate.holdsAt(InnerPredicate.java:1)
	at edu.udel.cis.vsl.minimp.search.DfsSearcher.search(DfsSearcher.java:105)
	at edu.udel.cis.vsl.minimp.search.DfsSearcher.search(DfsSearcher.java:93)
	at edu.udel.cis.vsl.minimp.verify.IF.OuterPredicate.holdsAt(OuterPredicate.java:188)
	at edu.udel.cis.vsl.minimp.verify.IF.OuterPredicate.holdsAt(OuterPredicate.java:1)
	at edu.udel.cis.vsl.minimp.search.DfsSearcher.search(DfsSearcher.java:105)
	at edu.udel.cis.vsl.minimp.search.DfsSearcher.search(DfsSearcher.java:93)
	at edu.udel.cis.vsl.minimp.verify.Comparison.compare(Comparison.java:82)
	at edu.udel.cis.vsl.minimp.verify.Comparison.compare(Comparison.java:29)
	at edu.udel.cis.vsl.minimp.MiniMP.compareEquivalence(MiniMP.java:468)
	at edu.udel.cis.vsl.minimp.MiniMP.main(MiniMP.java:487)
No violation at this state.
Writing specification trace to diffusion_seq.trace...done.
Writing implementation trace to diffusion1_par.trace...done.
Writing specification model to diffusion_seq.model...done.
Writing implementation model to diffusion1_par.model...done.

STATS:
   statesSeen    : 84 (spec) + 0 (impl) = 84
   statesMatched :  0 (spec) + 0 (impl) =  0
   statesSaved   : 84 (spec) + 0 (impl) = 84
   transitions   : 83 (spec) + 0 (impl) = 83
   time          : 2.783s.

RESULT: diffusion_seq and diffusion1_par MAY NOT be functionally equivalent. Counterexample found.
}}}
"	defect	closed	major		symbolic	1.0	fixed	class cast exception symbolic diffusion