TAPAAL

Exception thrown in editor during verification

Bug #1829887 reported by Asger Gitz-Johansen on 2019-05-21

This bug affects 1 person

Affects		Status	Importance	Assigned to	Milestone
	TAPAAL	Fix Released	Critical	Kenneth Yrke Jørgensen

Bug Description

When running the verifier on the attached tapn file, the following exception is thrown (after ~100 seconds):

Exception in thread "AWT-EventQueue-0" java.lang.IllegalArgumentException: Comparison method violates its general contract!

Related branches

lp:~yrke/tapaal/evenMore-gui-cleanup

Merged into lp:tapaal at revision 1078

Jiri Srba: Approve on 2020-08-10

Diff: 5542 lines (+1201/-1407)

106 files modified

build.gradle (+1/-0)
src/dk/aau/cs/approximation/OverApproximation.java (+2/-2)
src/dk/aau/cs/approximation/UnderApproximation.java (+3/-3)
src/dk/aau/cs/debug/Logger.java (+6/-2)
src/dk/aau/cs/gui/BatchProcessingDialog.java (+8/-8)
src/dk/aau/cs/gui/DeleteSharedPlaceOrTransition.java (+27/-19)
src/dk/aau/cs/gui/FileNameCellRenderer.java (+1/-1)
src/dk/aau/cs/gui/SharedPlacesAndTransitionsPanel.java (+26/-23)
src/dk/aau/cs/gui/TabContent.java (+488/-438)
src/dk/aau/cs/gui/TabTransformer.java (+2/-2)
src/dk/aau/cs/gui/TemplateExplorer.java (+0/-1)
src/dk/aau/cs/gui/components/ConstantsListModel.java (+1/-1)
src/dk/aau/cs/gui/components/EnabledTransitionsList.java (+4/-11)
src/dk/aau/cs/gui/components/NonsearchableJComboBox.java (+1/-1)
src/dk/aau/cs/gui/components/StatisticsPanel.java (+0/-1)
src/dk/aau/cs/gui/undo/AddFileBatchProcessingCommand.java (+3/-4)
src/dk/aau/cs/gui/undo/MoveElementDownCommand.java (+4/-7)
src/dk/aau/cs/gui/undo/MoveElementUpCommand.java (+4/-7)
src/dk/aau/cs/gui/undo/MovePlaceTransitionObject.java (+9/-13)
src/dk/aau/cs/gui/undo/RemoveFileBatchProcessingCommand.java (+2/-4)
src/dk/aau/cs/gui/undo/SortConstantsCommand.java (+2/-2)
src/dk/aau/cs/gui/undo/SortQueriesCommand.java (+1/-1)
src/dk/aau/cs/gui/undo/SortSharedPlacesCommand.java (+1/-1)
src/dk/aau/cs/gui/undo/SortSharedTransitionsCommand.java (+1/-1)
src/dk/aau/cs/gui/undo/SortTemplatesCommand.java (+4/-4)
src/dk/aau/cs/gui/undo/UpdateNameLabelOffsetCommand.java (+5/-2)
src/dk/aau/cs/io/LoadedModel.java (+6/-6)
src/dk/aau/cs/io/PNMLoader.java (+3/-4)
src/dk/aau/cs/io/TapnLegacyXmlLoader.java (+59/-68)
src/dk/aau/cs/io/TapnXmlLoader.java (+2/-4)
src/dk/aau/cs/io/TraceImportExport.java (+0/-1)
src/dk/aau/cs/model/NTA/trace/UppaalTrace.java (+3/-1)
src/dk/aau/cs/model/tapn/ConstantStore.java (+2/-2)
src/dk/aau/cs/model/tapn/LocalTimedMarking.java (+0/-1)
src/dk/aau/cs/model/tapn/NetworkMarking.java (+0/-1)
src/dk/aau/cs/model/tapn/TimeInterval.java (+3/-4)
src/dk/aau/cs/model/tapn/TimedArcPetriNet.java (+4/-4)
src/dk/aau/cs/model/tapn/TimedInputArc.java (+3/-3)
src/dk/aau/cs/model/tapn/TransportArc.java (+3/-3)
src/dk/aau/cs/model/tapn/simulation/ManualDelayMode.java (+1/-1)
src/dk/aau/cs/model/tapn/simulation/RandomDelayMode.java (+2/-2)
src/dk/aau/cs/model/tapn/simulation/ShortestDelayMode.java (+1/-1)
src/dk/aau/cs/model/tapn/simulation/TimedArcPetriNetTrace.java (+2/-1)
src/dk/aau/cs/model/tapn/simulation/TimedTAPNNetworkTrace.java (+2/-1)
src/dk/aau/cs/model/tapn/simulation/UntimedTAPNNetworkTrace.java (+3/-1)
src/dk/aau/cs/translations/tapn/BroadcastTranslation.java (+3/-3)
src/dk/aau/cs/translations/tapn/CombiTranslation.java (+3/-3)
src/dk/aau/cs/translations/tapn/Degree2BroadcastTranslation.java (+3/-3)
src/dk/aau/cs/translations/tapn/OptimizedStandardTranslation.java (+3/-3)
src/dk/aau/cs/translations/tapn/StandardTranslation.java (+3/-3)
src/dk/aau/cs/util/IntervalOperations.java (+11/-11)
src/dk/aau/cs/util/MemoryMonitor.java (+12/-33)
src/dk/aau/cs/verification/TAPNComposer.java (+4/-4)
src/dk/aau/cs/verification/VerificationResult.java (+1/-1)
src/net/tapaal/gui/DrawingSurfaceManager/AbstractDrawingSurfaceManager.java (+8/-3)
src/net/tapaal/resourcemanager/ResourceManager.java (+0/-2)
src/net/tapaal/swinghelpers/ExtendedJTabbedPane.java (+6/-2)
src/net/tapaal/swinghelpers/GridBagHelper.java (+82/-0)
src/pipe/dataLayer/Template.java (+0/-1)
src/pipe/gui/AnimationControlSidePanel.java (+1/-1)
src/pipe/gui/AnimationSettingsDialog.java (+0/-2)
src/pipe/gui/Animator.java (+1/-1)
src/pipe/gui/CreateGui.java (+28/-10)
src/pipe/gui/DelayEnabledTransitionControl.java (+1/-6)
src/pipe/gui/ExportBatchDialog.java (+5/-5)
src/pipe/gui/GuiFrame.java (+25/-77)
src/pipe/gui/GuiFrameController.java (+8/-4)
src/pipe/gui/Pipe.java (+6/-6)
src/pipe/gui/RunVerification.java (+0/-3)
src/pipe/gui/SelectionManager.java (+0/-1)
src/pipe/gui/action/GuiAction.java (+0/-1)
src/pipe/gui/action/SplitArcAction.java (+1/-1)
src/pipe/gui/canvas/Canvas.java (+0/-1)
src/pipe/gui/canvas/DrawingSurfaceImpl.java (+0/-2)
src/pipe/gui/canvas/PrototypeCanvas.java (+0/-1)
src/pipe/gui/graphicElements/AnnotationNote.java (+9/-5)
src/pipe/gui/graphicElements/Arc.java (+0/-3)
src/pipe/gui/graphicElements/Place.java (+10/-10)
src/pipe/gui/graphicElements/PlaceTransitionObject.java (+0/-1)
src/pipe/gui/graphicElements/tapn/TimedInputArcComponent.java (+0/-1)
src/pipe/gui/graphicElements/tapn/TimedPlaceComponent.java (+0/-2)
src/pipe/gui/graphicElements/tapn/TimedTransitionComponent.java (+1/-2)
src/pipe/gui/handler/ArcHandler.java (+0/-7)
src/pipe/gui/handler/PetriNetObjectHandler.java (+1/-24)
src/pipe/gui/handler/PlaceHandler.java (+0/-20)
src/pipe/gui/handler/TimedArcHandler.java (+0/-5)
src/pipe/gui/handler/TransitionHandler.java (+0/-23)
src/pipe/gui/undo/AddArcPathPointEdit.java (+3/-3)
src/pipe/gui/undo/AddTemplateCommand.java (+1/-1)
src/pipe/gui/undo/AnnotationBorderEdit.java (+1/-1)
src/pipe/gui/undo/AnnotationTextEdit.java (+3/-3)
src/pipe/gui/undo/ArcPathPointTypeEdit.java (+1/-1)
src/pipe/gui/undo/ArcTimeIntervalEdit.java (+4/-4)
src/pipe/gui/undo/TransitionRotationEdit.java (+2/-2)
src/pipe/gui/undo/TranslatePetriNetObjectEdit.java (+4/-4)
src/pipe/gui/undo/UndoManager.java (+6/-5)
src/pipe/gui/widgets/CTLQueryDialog.java (+16/-14)
src/pipe/gui/widgets/ConstantsDialogPanel.java (+25/-46)
src/pipe/gui/widgets/ConstantsPane.java (+10/-45)
src/pipe/gui/widgets/EngineDialogPanel.java (+16/-16)
src/pipe/gui/widgets/GuardDialogue.java (+13/-13)
src/pipe/gui/widgets/PlaceEditorPanel.java (+57/-143)
src/pipe/gui/widgets/QueryDialog.java (+12/-10)
src/pipe/gui/widgets/QueryPane.java (+6/-6)
src/pipe/gui/widgets/TAPNTransitionEditor.java (+80/-123)
src/pipe/gui/widgets/WorkflowDialog.java (+0/-2)

Revision history for this message

Asger Gitz-Johansen (sorenryge) wrote on 2019-05-21:

Note: This is a big autogenerated net, so the parser might take a while and all places/transitions are not positioned in a humanly readable manner Edit (760.4 KiB, text/xml)

Revision history for this message

Kenneth Yrke Jørgensen (yrke) wrote on 2020-07-22:

Download full text (6.0 KiB)

Full stack trace:

Full stack trace:

<code>
Exception in thread "AWT-EventQueue-0" java.lang.IllegalArgumentException: Comparison method violates its general contract!
	at java.base/java.util.TimSort.mergeLo(TimSort.java:781)
	at java.base/java.util.TimSort.mergeAt(TimSort.java:518)
	at java.base/java.util.TimSort.mergeCollapse(TimSort.java:448)
	at java.base/java.util.TimSort.sort(TimSort.java:245)
	at java.base/java.util.Arrays.sort(Arrays.java:1306)
	at java.base/java.util.ArrayList.sort(ArrayList.java:1720)
	at dk.aau.cs.verification.VerificationResult.getTransitionStatistics(VerificationResult.java:77)
	at pipe.gui.RunVerification.createMessagePanel(RunVerification.java:261)
	at pipe.gui.RunVerification.showResult(RunVerification.java:57)
	at pipe.gui.RunVerificationBase.done(RunVerificationBase.java:201)
	at java.desktop/javax.swing.SwingWorker$5.run(SwingWorker.java:750)
	at java.desktop/javax.swing.SwingWorker$DoSubmitAccumulativeRunnable.run(SwingWorker.java:847)
	at java.desktop/sun.swing.AccumulativeRunnable.run(AccumulativeRunnable.java:112)
	at java.desktop/javax.swing.SwingWorker$DoSubmitAccumulativeRunnable.actionPerformed(SwingWorker.java:857)
	at java.desktop/javax.swing.Timer.fireActionPerformed(Timer.java:317)
	at java.desktop/javax.swing.Timer$DoPostEvent.run(Timer.java:249)
	at java.desktop/java.awt.event.InvocationEvent.dispatch(InvocationEvent.java:316)
	at java.desktop/java.awt.EventQueue.dispatchEventImpl(EventQueue.java:770)
	at java.desktop/java.awt.EventQueue$4.run(EventQueue.java:721)
	at java.desktop/java.awt.EventQueue$4.run(EventQueue.java:715)
	at java.base/java.security.AccessController.doPrivileged(AccessController.java:391)
	at java.base/java.security.ProtectionDomain$JavaSecurityAccessImpl.doIntersectionPrivilege(ProtectionDomain.java:85)
	at java.desktop/java.awt.EventQueue.dispatchEvent(EventQueue.java:740)
	at java.desktop/java.awt.EventDispatchThread.pumpOneEventForFilters(EventDispatchThread.java:203)
	at java.desktop/java.awt.EventDispatchThread.pumpEventsForFilter(EventDispatchThread.java:124)
	at java.desktop/java.awt.EventDispatchThread.pumpEventsForFilter(EventDispatchThread.java:117)
	at java.desktop/java.awt.WaitDispatchSupport$2.run(WaitDispatchSupport.java:190)
	at java.desktop/java.awt.WaitDispatchSupport$4.run(WaitDispatchSupport.java:235)
	at java.desktop/java.awt.WaitDispatchSupport$4.run(WaitDispatchSupport.java:233)
	at java.base/java.security.AccessController.doPrivileged(AccessController.java:312)
	at java.desktop/java.awt.WaitDispatchSupport.enter(WaitDispatchSupport.java:233)
	at java.desktop/java.awt.Dialog.show(Dialog.java:1070)
	at java.desktop/java.awt.Component.show(Component.java:1717)
	at java.desktop/java.awt.Component.setVisible(Component.java:1664)
	at java.desktop/java.awt.Window.setVisible(Window.java:1023)
	at java.desktop/java.awt.Dialog.setVisible(Dialog.java:1005)
	at pipe.gui.Verifier.runVerifyTAPNVerification(Verifier.java:206)
	at pipe.gui.widgets.QueryPane.verifyQuery(QueryPane.java:480)
	at pipe.gui.widgets.QueryPane.lambda$addButtons$3(QueryPane.java:299)
	at java.desktop/javax.swing.AbstractButton.fireActionPerformed(AbstractButton.java:1967)
	at java.desktop/javax.swing.AbstractButton$Handler.actionPerformed(AbstractButton.java:2308)
	at java.desktop/javax.swing.DefaultButtonModel.fireActionPerformed(DefaultButtonModel.java:405)
	at java.desktop/javax.swing.DefaultButtonModel.setPressed(DefaultButtonModel.java:262)
	at java.desktop/javax.swing.plaf.basic.BasicButtonListener.mouseReleased(BasicButtonListener.java:279)
	at java.desktop/java.awt.AWTEventMulticaster.mouseReleased(AWTEventMulticaster.java:297)
	at java.desktop/java.awt.Component.processMouseEvent(Component.java:6636)
	at java.desktop/javax.swing.JComponent.processMouseEvent(JComponent.java:3342)
	at java.desktop/java.awt.Component.processEvent(Component.java:6401)
	at java.desktop/java.awt.Container.processEvent(Container.java:2263)
	at java.desktop/java.awt.Component.dispatchEventImpl(Component.java:5012)
	at java.desktop/java.awt.Container.dispatchEventImpl(Container.java:2321)
	at java.desktop/java.awt.Component.dispatchEvent(Component.java:4844)
	at java.desktop/java.awt.LightweightDispatcher.retargetMouseEvent(Container.java:4919)
	at java.desktop/java.awt.LightweightDispatcher.processMouseEvent(Container.java:4548)
	at java.desktop/java.awt.LightweightDispatcher.dispatchEvent(Container.java:4489)
	at java.desktop/java.awt.Container.dispatchEventImpl(Container.java:2307)
	at java.desktop/java.awt.Window.dispatchEventImpl(Window.java:2764)
	at java.desktop/java.awt.Component.dispatchEvent(Component.java:4844)
	at java.desktop/java.awt.EventQueue.dispatchEventImpl(EventQueue.java:772)
	at java.desktop/java.awt.EventQueue$4.run(EventQueue.java:721)
	at java.desktop/java.awt.EventQueue$4.run(EventQueue.java:715)
	at java.base/java.security.AccessController.doPrivileged(AccessController.java:391)
	at java.base/java.security.ProtectionDomain$JavaSecurityAccessImpl.doIntersectionPrivilege(ProtectionDomain.java:85)
	at java.base/java.security.ProtectionDomain$JavaSecurityAccessImpl.doIntersectionPrivilege(ProtectionDomain.java:95)
	at java.desktop/java.awt.EventQueue$5.run(EventQueue.java:745)
	at java.desktop/java.awt.EventQueue$5.run(EventQueue.java:743)
	at java.base/java.security.AccessController.doPrivileged(AccessController.java:391)
	at java.base/java.security.ProtectionDomain$JavaSecurityAccessImpl.doIntersectionPrivilege(ProtectionDomain.java:85)
	at java.desktop/java.awt.EventQueue.dispatchEvent(EventQueue.java:742)
	at java.desktop/java.awt.EventDispatchThread.pumpOneEventForFilters(EventDispatchThread.java:203)
	at java.desktop/java.awt.EventDispatchThread.pumpEventsForFilter(EventDispatchThread.java:124)
	at java.desktop/java.awt.EventDispatchThread.pumpEventsForHierarchy(EventDispatchThread.java:113)
	at java.desktop/java.awt.EventDispatchThread.pumpEvents(EventDispatchThread.java:109)
	at java.desktop/java.awt.EventDispatchThread.pumpEvents(EventDispatchThread.java:101)
	at java.desktop/java.awt.EventDispatchThread.run(EventDispatchThread.java:90)
</code>

Kenneth Yrke Jørgensen (yrke) on 2020-07-22

Changed in tapaal:
assignee:	nobody → Kenneth Yrke Jørgensen (yrke)
status:	New → In Progress

Kenneth Yrke Jørgensen (yrke) on 2020-07-22

Changed in tapaal:
importance:	Undecided → Critical

Jiri Srba (srba) on 2020-08-10

Changed in tapaal:
status:	In Progress → Fix Committed

Jiri Srba (srba) on 2020-11-01

Changed in tapaal:
status:	Fix Committed → Fix Released

Report a bug

This report contains Public information

Everyone can see this information.

You are

Subscribing...

Edit bug mail

Other bug subscribers

Bug attachments

Note: This is a big autogenerated net, so the parser might take a while and all places/transitions are not positioned in a humanly readable manner Edit

Add attachment

Remote bug watches

Bug watches keep track of this bug in other bug trackers.