Merge remote-tracking branch 'origin/master'

rt/src/main/java/edu/kit/iti/formal/psdbg/interpreter/dbg/StepIntoReverseCommand.java

@@ -15,6 +15,10 @@ public class StepIntoReverseCommand<T> extends DebuggerCommand<T> {
                 dbg.setStatePointer(statementBefore);
             } else{
                 dbg.setStatePointer(statePointer);
+
+                /*if (statePointer.isLastNode() || statePointer.isFirstNode()) {
+                    System.out.println("We need Sonderbehandlung here");
+                }*/
             }
         }
     }

rt/src/main/java/edu/kit/iti/formal/psdbg/interpreter/dbg/StepOverReverseCommand.java

@@ -6,14 +6,19 @@ public class StepOverReverseCommand<T> extends DebuggerCommand<T> {
     @Override
     public void execute(DebuggerFramework<T> dbg) throws DebuggerException {
         val statePointer = dbg.getCurrentStatePointer();
-        PTreeNode<T> stepOverReverse = statePointer.getStepInvInto() != null ?
-                statePointer.getStepInvInto() :
-                statePointer.getStepInvOver();
-
+        PTreeNode<T> stepOverReverse = statePointer.getStepInvOver();
         if (stepOverReverse == null) {
-            info("There is no previous state to the current one.");
-        }
-        dbg.setStatePointer(stepOverReverse);
+            int size = statePointer.getContextNodes().size();
+            dbg.setStatePointer(statePointer.getContextNodes().get(size - 1));
+            /*if(statePointer.isAtomic()) {
+                dbg.setStatePointer(statePointer);
+            }else{
+                info("There is no previous state to the current one.");
 
+            }*/
+            //state before statement
+        } else {
+            dbg.setStatePointer(stepOverReverse);
+        }
     }
 }

ui/src/main/java/edu/kit/iti/formal/psdbg/gui/controller/DebuggerMain.java

@@ -282,9 +282,11 @@ public class DebuggerMain implements Initializable {
      * @see {@link #handleStatePointer(PTreeNode)}
      */
     private void handleStatePointerUI(PTreeNode<KeyData> node) {
-        graph.addPartiallyAndMark(node);
+
 
         if (node != null) {
+            graph.addPartiallyAndMark(node);
+
             getInspectionViewsController().getActiveInspectionViewTab().activate(node, node.getStateBeforeStmt());
             scriptController.getDebugPositionHighlighter().highlight(node.getStatement());
         } else {
@@ -958,11 +960,22 @@ public class DebuggerMain implements Initializable {
     public void stepIntoReverse(ActionEvent actionEvent) {
         LOGGER.debug("DebuggerMain.stepIntoReverser");
         try {
-            if (model.getDebuggerFramework().getStatePointer().isAtomic()) {
-                model.getDebuggerFramework().getStatePointerListener()
-                        .add(new StepIntoReverseHandler(model.getStatePointer()));
+            PTreeNode<KeyData> statePointer = model.getDebuggerFramework().getStatePointer();
+            if (statePointer.getStepInvInto() == null) {
+                if (statePointer.getStepInvOver() != null) {
+                    if (statePointer.getStepInvOver().isAtomic()) {
+                        model.getDebuggerFramework().getStatePointerListener()
+                                .add(new StepIntoReverseHandler(model.getStatePointer()));
+                    }
+                    model.getDebuggerFramework().execute(new StepIntoReverseCommand<>());
+                } else {
+                    if (statePointer.isLastNode() || statePointer.isFirstNode()) {
+                        LOGGER.error("We need a special treatment");
+                    } else {
+                        LOGGER.error("There is no state to step into reverse");
+                    }
+                }
             }
-            model.getDebuggerFramework().execute(new StepIntoReverseCommand<>());
         } catch (DebuggerException e) {
             Utils.showExceptionDialog("", "", "", e);
             LOGGER.error(e);
@@ -1233,7 +1246,6 @@ public class DebuggerMain implements Initializable {
             Proof proof = beforeNode.getData().getProof();
 
             Node pnode = beforeNode.getData().getNode();
-            //      stateAfterStmt.forEach(keyDataGoalNode -> System.out.println("keyDataGoalNode.getData().getNode().serialNr() = " + keyDataGoalNode.getData().getNode().serialNr()));
 
             ptree.setProof(proof);
             ptree.setRoot(pnode);

ui/src/main/resources/edu/kit/iti/formal/psdbg/examples/contraposition/script.kps

 // Please select one of the following scripts.
 //
 
+script autoScript(){
+    auto;
+}
+
 script test1234(){
     impRight;
+    autoScript;
     //auto;
 }
 
 script test23(){
 impRight;
-x:term := find(match `?rt ==>`);
-impLeft formula=x;
-
+//x:term := find(match `?rt ==>`);
+//impLeft formula=x;
+impLeft formula=find(match `?rt ==>`);
 
 cases{
     case match `q==>`: