Commit 7b854843 authored by Sarah Grebing's avatar Sarah Grebing
Browse files

Framework for Testcases for proof tree

parent 14adebe7
Pipeline #23136 passed with stages
in 3 minutes and 22 seconds
......@@ -35,7 +35,11 @@ public class GoalNode<T> {
private int id = super.hashCode();
public GoalNode(T data) {
this(null, new VariableAssignment(), data, false);
this.assignments = new VariableAssignment();
this.parent = null;
this.data = data;
this.isClosed = false;
// this(null, new VariableAssignment(), data, false);
}
public GoalNode(@Nonnull GoalNode<T> parent, T data, boolean isClosed) {
......
......@@ -32,17 +32,19 @@ public class ProofTreeTest {
@Before
public void setUp() throws Exception {
facade = new KeYProofFacade();
scripts = Facade.getAST(CharStreams.fromStream(new FileInputStream("/home/sarah/Documents/KIT_Mitarbeiter/ProofScriptingLanguage/rt-key/src/test/resources/edu/kit/iti/formal/psdbg/interpreter/contraposition/proofTreeScript.kps")));
}
}
@Test
public void testScriptTree() throws IOException, ProblemLoaderException {
facade.loadKeyFileSync(new File("/home/sarah/Documents/KIT_Mitarbeiter/ProofScriptingLanguage/rt-key/src/test/resources/edu/kit/iti/formal/psdbg/interpreter/contraposition/contraposition.key"));
File keyProblem = new File(getClass().getResource("contraposition.key").getFile());
facade.loadKeyFileSync(keyProblem);
scripts = Facade.getAST(CharStreams.fromStream(getClass().getResourceAsStream("proofTreeScript.kps")));
InterpreterBuilder ib = facade.buildInterpreter();
i = ib.build();
DebuggerFramework<KeyData> df = new DebuggerFramework<>(i, scripts.get(0), null);
i.interpret(scripts.get(0));
ScriptTreeTransformation treeScriptCreation = new ScriptTreeTransformation(df.getPtreeManager(), facade.getProof(), facade.getProof().root());
treeScriptCreation.create(facade.getProof());
PTreeNode startNode = df.getPtreeManager().getStartNode();
......
// This file is part of KeY - Integrated Deductive Software Design
//
// Copyright (C) 2001-2011 Universitaet Karlsruhe (TH), Germany
// Universitaet Koblenz-Landau, Germany
// Chalmers University of Technology, Sweden
// Copyright (C) 2011-2013 Karlsruhe Institute of Technology, Germany
// Technical University Darmstadt, Germany
// Chalmers University of Technology, Sweden
//
// The KeY system is protected by the GNU General
// Public License. See LICENSE.TXT for details.
//
// Input file for KeY standalone prover version 0.497
\sorts {
s;
}
\predicates {
p;
q;
}
\problem {
(p -> q) -> !q -> !p
}
script full(){
impRight;
impRight;
impLeft;
cases {
case match `!q ==> p`:
notLeft;
notRight;
closeAntec;
case match `q==>!p`:
notLeft;
closeAntec;
}
}
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