LEGUP
LEGUP copied to clipboard
Bram-Hub
[BUG] Elimination rules throw exceptions when setting both the operator and the variable(s)
Description
Consider the following example for Not Elimination:
When trying to set both not and A to any combination of true or false and then selecting "Not Elimination", the following happens:
And the following errors show up in the terminal:
Exception in thread "AWT-EventQueue-0" java.lang.NullPointerException
at edu.rpi.legup.puzzle.shorttruthtable.rules.basic.DirectRule_Generic.checkRuleRawAt(DirectRule_Generic.java:43)
at edu.rpi.legup.model.rules.DirectRule.checkRuleAt(DirectRule.java:82)
at edu.rpi.legup.model.rules.DirectRule.checkRuleRaw(DirectRule.java:52)
at edu.rpi.legup.model.rules.DirectRule.checkRule(DirectRule.java:37)
at edu.rpi.legup.model.tree.TreeTransition.isCorrect(TreeTransition.java:337)
at edu.rpi.legup.model.tree.TreeTransition.isContradictoryBranch(TreeTransition.java:221)
at edu.rpi.legup.model.tree.TreeNode.isContradictoryBranch(TreeNode.java:36)
at edu.rpi.legup.ui.proofeditorui.treeview.TreeNodeView.draw(TreeNodeView.java:77)
at edu.rpi.legup.ui.proofeditorui.treeview.TreeView.redrawTree(TreeView.java:241)
at edu.rpi.legup.ui.proofeditorui.treeview.TreeView.drawTree(TreeView.java:424)
at edu.rpi.legup.ui.proofeditorui.treeview.TreeView.draw(TreeView.java:222)
at edu.rpi.legup.ui.ZoomablePane.paint(ZoomablePane.java:28)
at java.desktop/javax.swing.JComponent.paintChildren(JComponent.java:907)
at java.desktop/javax.swing.JComponent.paint(JComponent.java:1083)
at java.desktop/javax.swing.JViewport.paint(JViewport.java:737)
at java.desktop/javax.swing.JComponent.paintChildren(JComponent.java:907)
at java.desktop/javax.swing.JComponent.paint(JComponent.java:1083)
at java.desktop/javax.swing.JComponent.paintToOffscreen(JComponent.java:5255)
at java.desktop/javax.swing.RepaintManager$PaintManager.paintDoubleBufferedFPScales(RepaintManager.java:1707)
at java.desktop/javax.swing.RepaintManager$PaintManager.paintDoubleBuffered(RepaintManager.java:1616)
at java.desktop/javax.swing.RepaintManager$PaintManager.paint(RepaintManager.java:1556)
at java.desktop/javax.swing.RepaintManager.paint(RepaintManager.java:1323)
at java.desktop/javax.swing.JComponent._paintImmediately(JComponent.java:5203)
at java.desktop/javax.swing.JComponent.paintImmediately(JComponent.java:5013)
at java.desktop/javax.swing.RepaintManager$4.run(RepaintManager.java:865)
at java.desktop/javax.swing.RepaintManager$4.run(RepaintManager.java:848)
at java.base/java.security.AccessController.doPrivileged(Native Method)
at java.base/java.security.ProtectionDomain$JavaSecurityAccessImpl.doIntersectionPrivilege(ProtectionDomain.java:85)
at java.desktop/javax.swing.RepaintManager.paintDirtyRegions(RepaintManager.java:848)
at java.desktop/javax.swing.RepaintManager.paintDirtyRegions(RepaintManager.java:823)
at java.desktop/javax.swing.RepaintManager.prePaintDirtyRegions(RepaintManager.java:772)
at java.desktop/javax.swing.RepaintManager$ProcessingRunnable.run(RepaintManager.java:1890)
at java.desktop/java.awt.event.InvocationEvent.dispatch(InvocationEvent.java:313)
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(Native Method)
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.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)
Note that this also occurs for other elimination rules. See this screenshot for And Elimination:
Steps to Reproduce
- Download BlankNot.zip
- Unzip the file and open it in the proof editor
- Set not and A to any combination of true or false
- Attempt to justify this step with Not Elimination
- See a new node not appear, and there should be an exception thrown in the terminal
Expected Behavior
A new node should appear with a red transition arrow, as this is not a valid application of Not Elimination.
Screenshots
No response
Puzzle Files
Additional Context
Note that once this issue is fixed, the CannotSetBothAtOnceTest in src/test/java/puzzles/shorttruthtable/rules/NotEliminationTest.java should be uncommented. Additionally, it might be useful to generalize that test case for all Elimination rules.
Updated the description and title after doing some testing with Chase, this seems to be an issue across all Elimination rules.
Whoever works on this bug should uncomment the test case noted in #675.