Menu
▾
▴
#74 concurrent modification exception
Got it while typing / submitting a command to the prover that had a parsing error (I think).
It;s the first time this happens, but it isn't serious.
java.util.ConcurrentModificationException
at java.util.AbstractList$Itr.checkForComodification(AbstractList.java:372)
at java.util.AbstractList$Itr.next(AbstractList.java:343)
at net.sourceforge.czt.parser.util.ParseException.getMessage(ParseException.java:81)
at java.lang.Throwable.getLocalizedMessage(Throwable.java:267)
at java.lang.Throwable.toString(Throwable.java:343)
at java.lang.Throwable.<init>(Throwable.java:242)
at java.lang.Exception.<init>(Exception.java:77)
at net.sourceforge.czt.session.CommandException.<init>(CommandException.java:44)
at net.sourceforge.czt.parser.zeves.ParseUtils.doCompute(ParseUtils.java:399)
at net.sourceforge.czt.session.AbstractCommand.compute(AbstractCommand.java:52)
at net.sourceforge.czt.session.SectionManager.get(SectionManager.java:836)
at net.sourceforge.czt.parser.zeves.ParseUtils.parseExpr(ParseUtils.java:230)
at net.sourceforge.czt.eclipse.zeves.core.ZEvesResultConverter.parseZEvesExpr(ZEvesResultConverter.java:41)
at net.sourceforge.czt.eclipse.zeves.core.ZEvesResultConverter.parseZEvesResult(ZEvesResultConverter.java:62)
at net.sourceforge.czt.eclipse.zeves.core.ZEvesResultConverter.convert(ZEvesResultConverter.java:123)
at net.sourceforge.czt.eclipse.zeves.views.ZEditorResults$ZEvesProofObject.convertBlurbElement(ZEditorResults.java:410)
at net.sourceforge.czt.eclipse.zeves.views.ZEditorResults$ZEvesProofObject.loadContents(ZEditorResults.java:369)
at net.sourceforge.czt.eclipse.views.ZInfoView.loadContents(ZInfoView.java:525)
at net.sourceforge.czt.eclipse.views.ZInfoView$3.run(ZInfoView.java:462)
at org.eclipse.core.internal.jobs.Worker.run(Worker.java:54)
Ah, forgot to mention, the next command gave the warning that:
Cannot parse Z/Eves result:
line 1 column 27 in "StringSource": Expression expected; found predicate
Z/Eves result:
tdepth ((0, t)) = troots t ∧ tdepth ((1, t)) = dom (t ▷ tdepth ((0, t))) ∧ tdepth ((2, t)) = dom (t ▷ tdepth ((1, t))) ∧ tdepth ((3, t)) = dom (t ▷ tdepth ((2, t))) ∧ tdepth ((4, t)) = dom (t ▷ tdepth ((3, t))) ∧ tdepth ((5, t)) = dom (t ▷ tdepth ((4, t))) ∧ tdepth ((6, t)) = dom (t ▷ tdepth ((5, t))) ∧ t ∈ T → T0 ∧ x ∈ T ⇒ (∃ ss : { i : ℕ ⦁ tdepth ((i, t)) } ⦁ x ∈ ss)