Opened 16 years ago
Closed 16 years ago
#142 closed defect (fixed)
Class cast exception in diffusion1
| Reported by: | Stephen Siegel | Owned by: | ywei |
|---|---|---|---|
| Priority: | major | Milestone: | |
| Component: | symbolic | Version: | 1.0 |
| Keywords: | class cast exception symbolic diffusion | Cc: |
Description
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.
Change History (2)
comment:1 by , 16 years ago
| Status: | new → accepted |
|---|
comment:2 by , 16 years ago
| Resolution: | → fixed |
|---|---|
| Status: | accepted → closed |
Note:
See TracTickets
for help on using tickets.
Bug fixed in symbolic write expression and symbolic constant. They will not assume that they are comparing the same kind of expressions now. I am getting another exception when CVC3 tried to compare the output arrays of two programs. CVC3 will first check whether two arrays have the same dimensions before comparing the elements of the arrays. That cause the exception. Is it the correct way to comparing arrays?
The exception is as follows:
java.lang.RuntimeException: The dimension of SymRational[(X3+1)][X0] and the dimension of SymRational[X3][X0] are not equal.