Commit 035d0942 authored by Sarah Grebing's avatar Sarah Grebing
Browse files

Added bugfixes from master

parent fba5dd8e
Pipeline #17794 failed with stages
in 87 minutes and 13 seconds
......@@ -212,4 +212,4 @@ QUESTION_MARK: '?';
DIGITS : DIGIT+ ;
fragment DIGIT : [0-9] ;
ID : ([a-zA-Z]|'#') ([_a-zA-Z0-9] | '.' | '\\'| '#')*;
\ No newline at end of file
ID : ([a-zA-Z]|'#'|'_') ([_a-zA-Z0-9] | '.' | '\\'| '#')*;
\ No newline at end of file
......@@ -102,7 +102,7 @@ public class KeYMatcher implements MatcherApi<KeyData> {
* Match the label of a goal node
*
* @param currentState goal node as possible match cancidate
* @param label String representation for regualr expression for label to match
* @param label String representation for regular expression for label to match
* @return List of matches if match was sucessful, empty list otherwise
*/
@Override
......@@ -111,10 +111,17 @@ public class KeYMatcher implements MatcherApi<KeyData> {
List<VariableAssignment> assignments = new ArrayList<>();
resultsFromLabelMatch = new ArrayList<>();
//compile pattern
Pattern regexpForLabel = Pattern.compile(label);
String cleanLabel = label.replaceAll(" ", "");
String cleanLabel2 = cleanLabel.replaceAll("\\(", "\\\\(");
cleanLabel = cleanLabel2.replaceAll("\\)", "\\\\)");
String branchLabel = currentState.getData().getBranchingLabel();
Matcher branchLabelMatcher = regexpForLabel.matcher(branchLabel);
String cleanBranchLabel = branchLabel.replaceAll(" ", "");
Pattern regexpForLabel = Pattern.compile(cleanLabel);
Matcher branchLabelMatcher = regexpForLabel.matcher(cleanBranchLabel);
if (branchLabelMatcher.matches()) {
......@@ -160,16 +167,6 @@ public class KeYMatcher implements MatcherApi<KeyData> {
return assignments.isEmpty()? null: assignments;
}
private Value<String> toValueTerm(KeyData currentState, Term matched) {
String reprTerm = LogicPrinter.quickPrintTerm(matched, currentState.getEnv().getServices());
//Hack: to avoid newlines
String reprTermReformatted = reprTerm.trim();
return new Value<>(
new TermType(new SortType(matched.sort())),
reprTermReformatted
);
}
@Override
public List<VariableAssignment> matchSeq(GoalNode<KeyData> currentState,
String data,
......@@ -178,7 +175,7 @@ public class KeYMatcher implements MatcherApi<KeyData> {
//System.out.println("Signature " + sig.toString());
Matchings m = MatcherFacade.matches(data,
currentState.getData().getNode().sequent(), false, services);
currentState.getData().getNode().sequent(), false, currentState.getData().getProof().getServices());
if (m.isEmpty()) {
LOGGER.debug("currentState has no match= " + currentState.getData().getNode().sequent());
......@@ -208,6 +205,17 @@ public class KeYMatcher implements MatcherApi<KeyData> {
}
}
private Value<String> toValueTerm(KeyData currentState, Term matched) {
String reprTerm = LogicPrinter.quickPrintTerm(matched, currentState.getProof().getServices());
//Hack: to avoid newlines
String reprTermReformatted = reprTerm.trim();
return new Value<>(
new TermType(new SortType(matched.sort())),
reprTermReformatted
);
}
//private TermLiteral from(SequentFormula sf) {
// return new TermLiteral(sf.toString());
......
......@@ -16,5 +16,6 @@
<li><code>occ</code> : <em>INT</em> occurence of the top-level formula</li>
<li><code>with</code> : <em>TERM</em> the term with which variables should be instantiated</li>
</ul>
</body>
</html>
\ No newline at end of file
......@@ -73,5 +73,13 @@ public class KeYInterpreterTest {
}
@Test
public void testHookAssignments() throws IOException, ProblemLoaderException {
facade.loadKeyFileSync(new File("src/test/resources/edu/kit/iti/formal/psdbg/interpreter/contraposition/contraposition.key"));
Interpreter<KeyData> i = execute(getClass().getResourceAsStream("contraposition/hookTestScript.kps"));
Assert.assertTrue(i.isStrictMode());
}
}
script hookTest(){
__STRICT_MODE:= true;
impRight;
}
\ No newline at end of file
......@@ -140,6 +140,7 @@ public class Interpreter<T> extends DefaultASTVisitor<Object>
if (fireVariableAssignmentHook(node, var.getIdentifier(), v)) {
node.setVariableValue(var, v);
}
node.setVariableValue(var, v);
}
}
exitScope(assignmentStatement);
......
......@@ -39,7 +39,8 @@ public abstract class DefaultAssignmentHook<T> implements VariableAssignmentHook
Variable<T, S> variable = (Variable<T, S>) variables.get(variableName);
return variable.setter.apply(data, value);
}
return true;
//@AW: TODO was true: Why?
return false;
}
......
package edu.kit.iti.formal.psdbg.examples.lulu.bigIntProof;
import edu.kit.iti.formal.psdbg.examples.JavaExample;
import edu.kit.iti.formal.psdbg.examples.Example;
public class BigIntExample extends JavaExample {
public class BigIntExample extends Example {
public BigIntExample() {
setName("BigInt");
defaultInit(getClass());
}
}
......@@ -428,31 +428,51 @@ public class DebuggerMain implements Initializable {
executeScript(FACADE.buildInterpreter(), addInitBreakpoint);
}
/**
* Reload a problem from the beginning
*
* @param event
*/
@FXML
public void abortExecution() {
public void reloadProblem(ActionEvent event) {
//abort current execution();
//save old information and refresh models
statusBar.publishMessage("Reloading...");
File lastLoaded;
if (model.getKeyFile() != null) {
lastLoaded = model.getKeyFile();
} else {
Contract chosen = model.getChosenContract();
lastLoaded = model.getJavaFile();
}
//model.reload();
abortExecution();
Platform.runLater(() -> model.setStatePointer(null));
handleStatePointerUI(null);
if (model.getDebuggerFramework() != null) {
try {
// try to friendly
Future future = executorService.submit(() -> {
model.getDebuggerFramework().stop();
model.getDebuggerFramework().unregister();
model.getDebuggerFramework().release();
});
//reload getInspectionViewsController().getActiveInspectionViewTab().getModel()
InspectionModel iModel = getInspectionViewsController().getActiveInspectionViewTab().getModel();
//iModel.setHighlightedJavaLines(FXCollections.emptyObservableSet());
iModel.clearHighlightLines();
iModel.getGoals().clear();
iModel.setSelectedGoalNodeToShow(null);
// wait a second!
future.get(1, TimeUnit.SECONDS);
// urgently stop
model.getDebuggerFramework().hardStop();
} catch (InterruptedException | ExecutionException | TimeoutException e) {
e.printStackTrace();
} finally {
model.setDebuggerFramework(null);
try {
FACADE.reload(lastLoaded);
if (iModel.getGoals().size() > 0) {
iModel.setSelectedGoalNodeToShow(iModel.getGoals().get(0));
}
} else {
LOGGER.info("no interpreter running");
if (FACADE.getReadyToExecute()) {
LOGGER.info("Reloaded Successfully");
statusBar.publishMessage("Reloaded Sucessfully");
}
} catch (ProofInputException e) {
e.printStackTrace();
} catch (ProblemLoaderException e) {
e.printStackTrace();
}
assert model.getDebuggerFramework() == null;
}
@FXML
......@@ -768,44 +788,32 @@ public class DebuggerMain implements Initializable {
}
}
/**
* Reload a problem from the beginning
*
* @param event
*/
@FXML
public void reloadProblem(ActionEvent event) {
//abort current execution();
//save old information and refresh models
File lastLoaded;
if (model.getKeyFile() != null) {
lastLoaded = model.getKeyFile();
} else {
Contract chosen = model.getChosenContract();
lastLoaded = model.getJavaFile();
}
//model.reload();
abortExecution();
handleStatePointerUI(null);
model.setStatePointer(null);
//reload getInspectionViewsController().getActiveInspectionViewTab().getModel()
InspectionModel iModel = getInspectionViewsController().getActiveInspectionViewTab().getModel();
iModel.setHighlightedJavaLines(null);
iModel.getGoals().clear();
iModel.setSelectedGoalNodeToShow(null);
public void abortExecution() {
statusBar.publishMessage("Aborting Execution...");
if (model.getDebuggerFramework() != null) {
try {
// try to friendly
Future future = executorService.submit(() -> {
model.getDebuggerFramework().stop();
model.getDebuggerFramework().unregister();
model.getDebuggerFramework().release();
});
try {
FACADE.reload(lastLoaded);
if (iModel.getGoals().size() > 0) {
iModel.setSelectedGoalNodeToShow(iModel.getGoals().get(0));
// wait a second!
future.get(1, TimeUnit.SECONDS);
// urgently stop
model.getDebuggerFramework().hardStop();
} catch (InterruptedException | ExecutionException | TimeoutException e) {
e.printStackTrace();
} finally {
model.setDebuggerFramework(null);
statusBar.publishMessage("Execution aborted.");
}
} catch (ProofInputException e) {
e.printStackTrace();
} catch (ProblemLoaderException e) {
e.printStackTrace();
} else {
LOGGER.info("no interpreter running");
}
assert model.getDebuggerFramework() == null;
}
@FXML
......
......@@ -66,7 +66,7 @@ public class BaseCodeArea extends CodeArea {
final int start = lm.getLineStart(line);
final int end = lm.getLineEnd(line);
setStyle(start, end, Collections.singleton(clazz));
} catch (ArrayIndexOutOfBoundsException e) {
} catch (IndexOutOfBoundsException e) {
}
......
......@@ -56,10 +56,12 @@ public class JavaArea extends BaseCodeArea {
* highlight new lines
*/
private void highlightLineSet() {
linesToHighlightProperty().get().forEach(integer -> {
lineToClassProperty().get().put(integer - 1, "line-highlight");
});
highlightLines();
if (!linesToHighlight.get().isEmpty()) {
linesToHighlightProperty().get().forEach(integer -> {
lineToClassProperty().get().put(integer - 1, "line-highlight");
});
highlightLines();
}
}
private void updateView() {
......
......@@ -119,7 +119,6 @@ public class TacletContextMenu extends ContextMenu {
try {
ImmutableList<TacletApp> findTaclet = c.getFindTaclet(goal, occ);
createTacletMenu(
removeRewrites(findTaclet)
.prepend(c.getRewriteTaclet(goal, occ)),
......
......@@ -295,7 +295,9 @@ public class Utils {
grid.add(new Label("Interpreter finished successfully"), 0, 0);
String msg = String.format("%s %d %s ", "There were still", noOfGoals,
"open goals.");
String msg2 = "You can continue the proof interactively by using the interactive button.\nThis enables to point and click onto the sequents and apply rules";
String msg2 = "You can continue the proof interactively by using the interactive button.\n" +
"This enables to point and click onto the sequents and apply rules\n"
+ "Applying splitting rules interactively is currently not supported yet.";
grid.add(new Label(msg), 0, 1);
grid.add(new MaterialDesignIconView(MaterialDesignIcon.HAND_POINTING_RIGHT, "24.0"), 3, 1);
......
......@@ -162,6 +162,9 @@ public class InspectionModel {
return isInterpreterTab;
}
public void clearHighlightLines() {
highlightedJavaLinesProperty().clear();
}
enum Mode {
LIVING, DEAD, POSTMORTEM,
......
......@@ -2,6 +2,9 @@
//
script autoScript(){
__KEY_NON_LINEAR_ARITHMETIC := 'defops';
__STRICT_MODE := true;
auto;
}
......@@ -16,8 +19,8 @@ script interactive_with_match(){
impRight;
impLeft;
cases{
case match `?X -> ?Y ==> not(?Z)`:
notLeft;
case match ` not(?Z)==>`:
notLeft;;
default:
notRight;
}
......
Markdown is supported
0% or .
You are about to add 0 people to the discussion. Proceed with caution.
Finish editing this message first!
Please register or to comment