Commit 361e39ae authored by Lulu Luong's avatar Lulu Luong

added test cases

changed IndistintWindow to IndistinctInformation, because we'll be using dialogs instead of seperate windows
added Countdownlatch for synchronziation
Bug fixes for the ScriptTree
parent 6d75608b
Pipeline #42041 passed with stages
in 5 minutes and 42 seconds
......@@ -8,11 +8,11 @@ import de.uka.ilkd.key.java.Services;
import de.uka.ilkd.key.proof.Goal;
import de.uka.ilkd.key.proof.Proof;
import de.uka.ilkd.key.proof.init.ProofInputException;
import de.uka.ilkd.key.proof.init.ProofOblInput;
import de.uka.ilkd.key.proof.io.ProblemLoaderException;
import de.uka.ilkd.key.speclang.Contract;
import edu.kit.iti.formal.psdbg.interpreter.data.GoalNode;
import edu.kit.iti.formal.psdbg.interpreter.data.KeyData;
import edu.kit.iti.formal.psdbg.interpreter.funchdl.TacletAppSelectionDialogService;
import javafx.beans.binding.BooleanBinding;
import javafx.beans.property.SimpleBooleanProperty;
import javafx.beans.property.SimpleObjectProperty;
......
......@@ -3,16 +3,12 @@ package edu.kit.iti.formal.psdbg.interpreter;
import com.google.common.collect.BiMap;
import com.google.common.collect.ImmutableBiMap;
import de.uka.ilkd.key.api.VariableAssignments;
import de.uka.ilkd.key.java.Services;
import de.uka.ilkd.key.logic.Term;
import de.uka.ilkd.key.logic.TermBuilder;
import de.uka.ilkd.key.parser.ParserException;
import de.uka.ilkd.key.proof.Node;
import de.uka.ilkd.key.proof.Proof;
import edu.kit.iti.formal.psdbg.interpreter.data.*;
import edu.kit.iti.formal.psdbg.interpreter.exceptions.InvalidTypeException;
import edu.kit.iti.formal.psdbg.interpreter.funchdl.CommandLookup;
import edu.kit.iti.formal.psdbg.interpreter.matcher.KeYMatcher;
import edu.kit.iti.formal.psdbg.interpreter.funchdl.TacletAppSelectionDialogService;
import edu.kit.iti.formal.psdbg.parser.Visitor;
import edu.kit.iti.formal.psdbg.parser.ast.*;
import edu.kit.iti.formal.psdbg.parser.data.Value;
......@@ -22,7 +18,6 @@ import edu.kit.iti.formal.psdbg.parser.types.TypeFacade;
import lombok.Getter;
import lombok.Setter;
import java.util.Collections;
import java.util.List;
import java.util.function.Function;
......
......@@ -17,17 +17,14 @@ import de.uka.ilkd.key.proof.Proof;
import de.uka.ilkd.key.proof.RuleAppIndex;
import de.uka.ilkd.key.proof.SVInstantiationException;
import de.uka.ilkd.key.proof.rulefilter.TacletFilter;
import de.uka.ilkd.key.rule.IfFormulaInstantiation;
import de.uka.ilkd.key.rule.Rule;
import de.uka.ilkd.key.rule.Taclet;
import de.uka.ilkd.key.rule.TacletApp;
import de.uka.ilkd.key.rule.inst.InstantiationEntry;
import de.uka.ilkd.key.rule.inst.SVInstantiations;
import edu.kit.iti.formal.psdbg.RuleCommandHelper;
import edu.kit.iti.formal.psdbg.ValueInjector;
import edu.kit.iti.formal.psdbg.interpreter.IndistinctWindow;
import edu.kit.iti.formal.psdbg.interpreter.IndistinctInformation;
import edu.kit.iti.formal.psdbg.interpreter.Interpreter;
import edu.kit.iti.formal.psdbg.interpreter.TacletAppSelectionDialogService;
import edu.kit.iti.formal.psdbg.interpreter.data.GoalNode;
import edu.kit.iti.formal.psdbg.interpreter.data.KeyData;
import edu.kit.iti.formal.psdbg.interpreter.data.State;
......@@ -35,36 +32,20 @@ import edu.kit.iti.formal.psdbg.interpreter.data.VariableAssignment;
import edu.kit.iti.formal.psdbg.interpreter.exceptions.ScriptCommandNotApplicableException;
import edu.kit.iti.formal.psdbg.interpreter.exceptions.VariableNotDeclaredException;
import edu.kit.iti.formal.psdbg.interpreter.exceptions.VariableNotDefinedException;
import edu.kit.iti.formal.psdbg.parser.Facade;
import edu.kit.iti.formal.psdbg.parser.ast.*;
import javafx.collections.FXCollections;
import javafx.collections.ObservableList;
import javafx.event.ActionEvent;
import javafx.event.EventHandler;
import javafx.geometry.Pos;
import javafx.scene.Scene;
import javafx.scene.control.Button;
import javafx.scene.control.ListView;
import javafx.scene.control.TextField;
import javafx.scene.layout.VBox;
import javafx.stage.Modality;
import javafx.stage.Stage;
import javafx.stage.StageStyle;
import lombok.Getter;
import lombok.RequiredArgsConstructor;
import lombok.Setter;
import org.apache.logging.log4j.LogManager;
import org.apache.logging.log4j.Logger;
import org.key_project.util.collection.DefaultImmutableMap;
import org.key_project.util.collection.ImmutableList;
import org.key_project.util.collection.ImmutableMap;
import org.key_project.util.collection.ImmutableMapEntry;
import java.io.IOException;
import java.math.BigInteger;
import java.util.*;
import java.util.concurrent.BrokenBarrierException;
import java.util.concurrent.CyclicBarrier;
import java.util.concurrent.CountDownLatch;
/**
* @author Alexander Weigl
......@@ -194,20 +175,19 @@ public class RuleCommandHandler implements CommandHandler<KeyData> {
int linenr = call.getStartPosition().getLineNumber();
completed_matchingapps.forEach(k -> obsMatchApps.add(tacletAppIntoString(k, kd.getGoal(), linenr)));
//open window here
CyclicBarrier cyclicBarrier = new CyclicBarrier(2, tacletAppSelectionDialogService.getRunnable());
IndistinctWindow indistinctWindow = new IndistinctWindow(obsMatchApps);
CountDownLatch countDownLatch = new CountDownLatch(1);
tacletAppSelectionDialogService.setCyclicBarrier(cyclicBarrier);
tacletAppSelectionDialogService.setPane(indistinctWindow);
//open window here
tacletAppSelectionDialogService.makeRunnable();
tacletAppSelectionDialogService.setCountDownLatch(countDownLatch);
IndistinctInformation indistinctInformation = new IndistinctInformation(obsMatchApps);
tacletAppSelectionDialogService.setErrorInformation(indistinctInformation);
tacletAppSelectionDialogService.showDialog();
try {
cyclicBarrier.await();
} catch (InterruptedException ex) {
} catch (BrokenBarrierException ex) {
countDownLatch.await();
} catch (InterruptedException e1) {
e1.printStackTrace();
}
TacletApp chosenApp = completed_matchingapps.get(tacletAppSelectionDialogService.getUserIndexInput());
......
package edu.kit.iti.formal.psdbg.interpreter.funchdl;
import edu.kit.iti.formal.psdbg.interpreter.ErrorInformation;
import edu.kit.iti.formal.psdbg.interpreter.IndistinctInformation;
import javafx.application.Platform;
import javafx.scene.control.ChoiceDialog;
import lombok.Getter;
import lombok.Setter;
import java.util.List;
import java.util.Optional;
import java.util.concurrent.*;
public abstract class TacletAppSelectionDialogService {
@Setter
ErrorInformation errorInformation;
@Setter
CountDownLatch countDownLatch;
@Getter
int userIndexInput;
@Getter
private Runnable runnable;
public void showDialog() {
Platform.runLater(runnable);
}
public void makeRunnable() {
runnable = new Runnable() {
@Override
public void run() {
if (errorInformation instanceof IndistinctInformation) {
List tacletApps = ((IndistinctInformation) errorInformation).getMatchApps();
ChoiceDialog<String> dialog = new ChoiceDialog<>(tacletApps.get(0), tacletApps);
dialog.setTitle("Indistinct taclet application:");
dialog.setHeaderText("Choose a taclet application:");
dialog.setContentText("Possible taclet applications:");
// Traditional way to get the response value.
Optional<String> result = dialog.showAndWait();
result.ifPresent(tacletApp -> {
userIndexInput = tacletApps.indexOf(tacletApp);
countDownLatch.countDown();
});
}
}
};
}
}
package edu.kit.iti.formal.psdbg.interpreter;
/**
* Interface for classes that model information for completing a taclet application
*/
public interface ErrorInformation {
}
package edu.kit.iti.formal.psdbg.interpreter;
import javafx.collections.ObservableList;
import lombok.Getter;
/**
* Contains information
*/
public class IndistinctInformation implements ErrorInformation {
@Getter
ObservableList<String> matchApps;
public IndistinctInformation(ObservableList<String> matchApps) {
this.matchApps = matchApps;
}
}
package edu.kit.iti.formal.psdbg.interpreter;
import javafx.collections.ObservableList;
import javafx.event.EventHandler;
import javafx.fxml.FXMLLoader;
import javafx.geometry.Orientation;
import javafx.scene.control.Button;
import javafx.scene.control.ListView;
import javafx.scene.control.ScrollPane;
import javafx.scene.control.TextField;
import javafx.scene.input.MouseEvent;
import javafx.scene.layout.BorderPane;
import javafx.scene.layout.FlowPane;
import javafx.scene.layout.HBox;
import javafx.scene.layout.VBox;
import javafx.scene.text.Text;
import lombok.Getter;
import java.util.List;
public class IndistinctWindow extends VBox {
@Getter
int indexOfSelected = -1;
public Button accept;
public IndistinctWindow(ObservableList<String> matchApps) {
this.setPrefWidth(700);
//Center
ListView<String> listView = new ListView<String>(matchApps);
this.getChildren().add(listView);
//Bottom
accept = new Button();
accept.setText("Accept");
this.getChildren().add(accept);
listView.setOnMouseClicked(new EventHandler<MouseEvent>() {
@Override
public void handle(MouseEvent event) {
indexOfSelected = listView.getSelectionModel().getSelectedIndex();
}
});
}
}
package edu.kit.iti.formal.psdbg.interpreter;
import javafx.application.Platform;
import javafx.concurrent.Service;
import javafx.concurrent.Task;
import javafx.event.EventHandler;
import javafx.fxml.FXML;
import javafx.fxml.FXMLLoader;
import javafx.scene.Scene;
import javafx.scene.control.Button;
import javafx.scene.control.Dialog;
import javafx.scene.input.MouseEvent;
import javafx.scene.layout.BorderPane;
import javafx.scene.layout.Pane;
import javafx.stage.Stage;
import lombok.Getter;
import lombok.Setter;
import java.util.List;
import java.util.Optional;
import java.util.concurrent.*;
public abstract class TacletAppSelectionDialogService {
@Setter
IndistinctWindow pane;
@Getter
int userIndexInput;
private Runnable runnable;
@Setter
private CyclicBarrier cyclicBarrier;
public void showDialog() {
runnable = getRunnable();
Platform.runLater(runnable);
}
public Runnable getRunnable() {
return () -> {
if (pane != null) {
Dialog<Object> stage = new Dialog<>();
stage.setTitle("TacletAppSelectionDialog");
//Scene scene = new Scene(pane);
stage.getDialogPane().setContent(pane);
Optional<Object> app = stage.showAndWait();
try {
stage.close();
cyclicBarrier.await();
} catch (InterruptedException | BrokenBarrierException ignored) {
}
}
};
}
private void getIndex() {
userIndexInput = ((IndistinctWindow) pane).getIndexOfSelected();
}
}
......@@ -20,7 +20,6 @@ import edu.kit.iti.formal.psdbg.examples.Examples;
import edu.kit.iti.formal.psdbg.fmt.DefaultFormatter;
import edu.kit.iti.formal.psdbg.gui.ProofScriptDebugger;
import edu.kit.iti.formal.psdbg.gui.controls.*;
import edu.kit.iti.formal.psdbg.gui.controls.ScriptTree.AbstractTreeNode;
import edu.kit.iti.formal.psdbg.gui.graph.Graph;
import edu.kit.iti.formal.psdbg.gui.graph.GraphView;
import edu.kit.iti.formal.psdbg.gui.model.DebuggerMainModel;
......@@ -30,20 +29,21 @@ import edu.kit.iti.formal.psdbg.gui.model.MainScriptIdentifier;
import edu.kit.iti.formal.psdbg.interpreter.InterpreterBuilder;
import edu.kit.iti.formal.psdbg.interpreter.KeYProofFacade;
import edu.kit.iti.formal.psdbg.interpreter.KeyInterpreter;
import edu.kit.iti.formal.psdbg.interpreter.TacletAppSelectionDialogService;
import edu.kit.iti.formal.psdbg.interpreter.funchdl.TacletAppSelectionDialogService;
import edu.kit.iti.formal.psdbg.interpreter.data.GoalNode;
import edu.kit.iti.formal.psdbg.interpreter.data.KeyData;
import edu.kit.iti.formal.psdbg.interpreter.data.SavePoint;
import edu.kit.iti.formal.psdbg.interpreter.data.State;
import edu.kit.iti.formal.psdbg.interpreter.dbg.*;
import edu.kit.iti.formal.psdbg.parser.ASTDiff;
import edu.kit.iti.formal.psdbg.parser.Facade;
import edu.kit.iti.formal.psdbg.parser.ast.ASTNode;
import edu.kit.iti.formal.psdbg.parser.ast.ProofScript;
import edu.kit.iti.formal.psdbg.storage.KeyPersistentFacade;
import javafx.application.Platform;
import javafx.beans.InvalidationListener;
import javafx.beans.binding.BooleanBinding;
import javafx.beans.value.ChangeListener;
import javafx.beans.value.ObservableValue;
import javafx.collections.FXCollections;
import javafx.collections.ObservableList;
import javafx.concurrent.Service;
......@@ -417,6 +417,12 @@ public class DebuggerMain implements Initializable {
scriptExecutionController = new ScriptExecutionController(this);
renewThreadStateTimer();
model.statePointerProperty().addListener(new ChangeListener<PTreeNode<KeyData>>() {
@Override
public void changed(ObservableValue<? extends PTreeNode<KeyData>> observable, PTreeNode<KeyData> oldValue, PTreeNode<KeyData> newValue) {
refreshScriptTreeView();
}
});
savePointController = new SavePointController(this);
viewSettings = new ViewSettings(this);
......@@ -1380,16 +1386,6 @@ public class DebuggerMain implements Initializable {
}
}
@FXML
public void showUserInteractionW(ActionEvent actionEvent) {
Stage stage = new Stage();
stage.setTitle("Userinteraction");
Scene scene = new Scene(new UserinteractionWindow());
stage.setScene(scene);
stage.show();
}
@FXML
public void showViewSettings(ActionEvent actionEvent) {
Stage stage = new Stage();
......
......@@ -547,13 +547,7 @@ public class InteractiveModeController {
} catch (Exception e) {
if (e.getClass().equals(ScriptException.class)) {
if (e.getMessage().equals("Not a unique \\assumes instantiation")) {
//TODO: open UserinteractionWindow
//TODO: apply completed TacletApp
//TODO: insert into script
}
System.out.println("e.getMessage() = " + e.getMessage());
throw new ScriptCommandNotApplicableException(e, c, map);
......
......@@ -12,18 +12,10 @@ import edu.kit.iti.formal.psdbg.interpreter.data.State;
import edu.kit.iti.formal.psdbg.interpreter.dbg.PTreeNode;
import edu.kit.iti.formal.psdbg.parser.DefaultASTVisitor;
import edu.kit.iti.formal.psdbg.parser.ast.*;
import javafx.beans.property.MapProperty;
import javafx.beans.property.SimpleMapProperty;
import javafx.collections.FXCollections;
import javafx.scene.control.TreeCell;
import javafx.scene.control.TreeItem;
import javafx.scene.control.TreeView;
import javafx.scene.control.cell.TextFieldTreeCell;
import javafx.util.StringConverter;
import lombok.Getter;
import lombok.Setter;
import javax.annotation.Nullable;
import java.util.*;
......@@ -142,7 +134,7 @@ public class ScriptTreeGraph {
}
List<AbstractTreeNode> subchild = new ArrayList<>();
subchild.add(atn);
//TODO: Hack for double foreach-end recognition
if(atn.getParent() == childlist.get(0).getParent()) return;
childlist.get(0).setChildren(subchild);
}
......@@ -171,8 +163,14 @@ public class ScriptTreeGraph {
*/
private void computeList () {
while (currentNode != null) {
// already executed by interpreter
if (currentNode.getStateAfterStmt() != null) {
sortedList.add(currentNode);
currentNode = currentNode.getNextPtreeNode(currentNode);
} else { // not executed by interpreter yet
break;
}
}
}
......@@ -198,57 +196,6 @@ public class ScriptTreeGraph {
mapping.size();
}
/*
public TreeItem<AbstractTreeNode> toView () {
TreeItem<AbstractTreeNode> treeItem;
if(rootNode == null) {
treeItem = new TreeItem<>(new AbstractTreeNode(null));
DummyGoalNode dummy = new DummyGoalNode(null, false);
treeItem.getChildren().add(new TreeItem<>(dummy));
return treeItem;
}
treeItem = new TreeItem<>(new AbstractTreeNode(null));
List<AbstractTreeNode> children = mapping.get(rootNode.getNode()).getChildren();
if (children == null) return treeItem;
treeItem.getChildren().add(new TreeItem<>(mapping.get(rootNode.getNode())));
while (children.size() == 1) {
treeItem.getChildren().add(new TreeItem<>(children.get(0)));
children = children.get(0).getChildren();
if(children == null) return treeItem;
}
if (children.size() != 0) {
children.forEach(k -> treeItem.getChildren().add(rekursiveToView(k)));
}
return treeItem;
}
private TreeItem<AbstractTreeNode> rekursiveToView (AbstractTreeNode current){
TreeItem<AbstractTreeNode> treeItem = new TreeItem<>(current); //
List<AbstractTreeNode> children = current.getChildren();
while (children != null && children.size() == 1) {
if(children.get(0) == null) return treeItem;
treeItem.getChildren().add(new TreeItem<>(children.get(0)));
children = children.get(0).getChildren();
}
if (children == null) {
return treeItem;
}
if (children.size() != 0) {
children.forEach(k -> treeItem.getChildren().add(rekursiveToView(k)));
}
return treeItem;
}
*/
private class ScriptVisitor extends DefaultASTVisitor<Void> {
@Override
......@@ -259,6 +206,7 @@ public class ScriptTreeGraph {
Node callnode = nextPtreeNode.getStateBeforeStmt().getSelectedGoalNode().getData().getNode();
ScriptTreeNode sn = new ScriptTreeNode(callnode, nextPtreeNode, nextPtreeNode.getStatement().getStartPosition().getLineNumber());
//check if statement was applicable
if (nextPtreeNode.getStateAfterStmt().getGoals().equals(nextPtreeNode.getStateBeforeStmt().getGoals())) {
sn.setSucc(false);
}
......@@ -279,7 +227,7 @@ public class ScriptTreeGraph {
addPlaceholder(sn, sn.getNode());
break;
case 1:
// putIntoMapping(children.get(0).getData().getNode(), null);
putIntoFront(children.get(0).getData().getNode());
addPlaceholder(sn, children.get(0).getData().getNode());
break;
......@@ -344,8 +292,6 @@ public class ScriptTreeGraph {
@Override
public Void visit(DefaultCaseStatement caseStatement) {
PTreeNode<KeyData> nextintoptn = nextPtreeNode.getStepInto();
//TODO: QS throws a Nullpointer at same point, eventhough cript has no Defaultstatement
ScriptTreeNode match = new ScriptTreeNode(nextPtreeNode.getStepInto().getStateBeforeStmt().getSelectedGoalNode().getData().getNode(),nextPtreeNode, nextPtreeNode.getStatement().getStartPosition().getLineNumber());
match.setMatchEx(true);
match.setSucc(true);
......@@ -634,11 +580,14 @@ public class ScriptTreeGraph {
return -1;
}
/**
* Replace all placeholders with Dummygoals and count number of open and closed goals for statistics
* Count number of oben
*/
private void addGoals() {
//No script has been executed yet
if (rootNode instanceof DummyGoalNode) {
//fill statitics
//fill statistics
if (rootNode.getNode().isClosed()) {
closedGoals++;
} else {
......
......@@ -104,15 +104,23 @@ public class ScriptTreeView extends BorderPane {
TreeItem<AbstractTreeNode> treeItem = new TreeItem<>(new AbstractTreeNode(null));
rootNode = stg.getRootNode();
mapping = stg.getMapping();
if (rootNode instanceof DummyGoalNode) {
treeItem.getChildren().add(new TreeItem<>(rootNode));
this.setTree(treeItem);
return;
}
mapping = stg.getMapping();
// first scriptcommand not executed yet
if (mapping.get(rootNode.getNode()) == null) {
treeItem.getChildren().add(new TreeItem<>(new DummyGoalNode(rootNode.getNode(), rootNode.getNode().isClosed())));
this.setTree(treeItem);
return;
}
List<AbstractTreeNode> children = mapping.get(rootNode.getNode()).getChildren();
if (children == null) {
this.setTree(treeItem);
return;
......
package edu.kit.iti.formal.psdbg.gui.controls;
import javafx.fxml.FXML;
import javafx.scene.control.Button;
import javafx.scene.control.TextArea;
import javafx.scene.layout.BorderPane;
public class UserinteractionWindow extends BorderPane {
@FXML
Button cancelButton;
@FXML
Button applyButton;
@FXML
TextArea tacletDescription;
public UserinteractionWindow() {
Utils.createWithFXML(this);
}
}
......@@ -65,7 +65,6 @@ public class VariableAssignmentWindow extends BorderPane {
public VariableAssignmentWindow(InspectionModel inspectionModel) {
//TODO: reduce size of constructor
Utils.createWithFXML(this);
this.inspectionModel = inspectionModel;
......@@ -165,6 +164,13 @@ public class VariableAssignmentWindow extends BorderPane {
}
});
watches_tableView.setRowFactory(tv -> new TableRow<VariableModel>() {
@Override
protected void updateItem(VariableModel vm, boolean empty) {
setStyle("-fx-background-color: white;");
}
});
inspectionModel.currentInterpreterGoalProperty().addListener(new ChangeListener<GoalNode<KeyData>>() {
@Override
public void changed(ObservableValue<? extends GoalNode<KeyData>> observable, GoalNode<KeyData> oldValue, GoalNode<KeyData> newValue) {
......@@ -239,23 +245,31 @@ public class VariableAssignmentWindow extends BorderPane {
matchexp = match_variables.getText();
if (matchexp.equals("")) return;
Value value;
VariableModel vm;
try {
value = evaluator.eval(Facade.parseExpression(matchexp));
VariableModel vm = new VariableModel(matchexp,
vm = new VariableModel(matchexp,
value.getType().toString(),
value.getData().toString());
} catch (Exception e) {
System.out.println("No evaluable expression");
vm = new VariableModel(matchexp,
"NOT DEFINED",
"NOT DEFINED");
}
watchesModel.add(vm);
watches_tableView.refresh();
//focus on tab
SingleSelectionModel<Tab> selectionModel = tabPane.getSelectionModel();
selectionModel.select(watchesTab);
} catch (Exception e) {
System.out.println("No evaluable expression");
}
}
/**
......
// for testing the IndistinctWindow
script mock_interaction() {
impRight;
andLeft;
andLeft;
applyEq;
}
script interaction() {
impRight;
andLeft;
andLeft;
// apply 'applyEq' on 'a' in 'a = d'
}