Merge remote-tracking branch 'origin/master'

# Conflicts:
#	lang/src/main/java/edu/kit/iti/formal/psdbg/parser/TransformAst.java

lang/src/main/antlr4/edu/kit/iti/formal/psdbg/parser/ScriptLanguage.g4

@@ -28,12 +28,11 @@ stmtList
 
 statement
     :   //scriptDecl
-         assignment
-    |   repeatStmt
-    |   casesStmt
-    |   forEachStmt
-    |   theOnlyStmt
-    |   scriptCommand
+      assignment
+    | casesStmt
+    | scriptCommand
+    | unconditionalBlock
+    | conditionalBlock
   //  |   callStmt
     ;
 
@@ -102,10 +101,6 @@ scriptVar
     ;
 
 
-repeatStmt
-    :   REPEAT INDENT stmtList DEDENT
-    ;
-
 casesStmt
     :   CASES INDENT
             casesList*
@@ -126,12 +121,12 @@ casesList
     : CLOSES  INDENT closesGuard=stmtList DEDENT
     ;*/
 
-forEachStmt
-    :   FOREACH INDENT stmtList DEDENT
+unconditionalBlock
+    : (kind+=(FOREACH|THEONLY|STRICT|RELAX|REPEAT))+ INDENT stmtList DEDENT
     ;
 
-theOnlyStmt
-    :   THEONLY INDENT stmtList DEDENT
+conditionalBlock
+    : kind=(IF|WHILE) LPAREN expression RPAREN INDENT stmtList DEDENT
     ;
 
 
@@ -176,14 +171,16 @@ BOOL: 'bool' ;
 TERMTYPE : 'term' ;*/
 FOREACH : 'foreach' ;
 THEONLY : 'theonly' ;
+STRICT : 'strict' ;
+RELAX : 'relax';
+IF:'if';
+WHILE:'while';
 INDENT : '{' ;
 DEDENT : '}' ;
 SEMICOLON : ';' ;
 COLON : ':' ;
-HEAPSIMP:'heap-simp';
 SUBST_TO: '\\';
 
-
 STRING_LITERAL
    : '\'' ('\'\'' | ~ ('\''))* '\''
    ;

lang/src/main/java/edu/kit/iti/formal/psdbg/parser/ASTTraversal.java

 package edu.kit.iti.formal.psdbg.parser;
 
-/*-
- * #%L
- * ProofScriptParser
- * %%
- * Copyright (C) 2017 Application-oriented Formal Verification
- * %%
- * This program is free software: you can redistribute it and/or modify
- * it under the terms of the GNU General default License as
- * published by the Free Software Foundation, either version 3 of the
- * License, or (at your option) any later version.
- * 
- * This program is distributed in the hope that it will be useful,
- * but WITHOUT ANY WARRANTY; without even the implied warranty of
- * MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE.  See the
- * GNU General default License for more details.
- * 
- * You should have received a copy of the GNU General default
- * License along with this program.  If not, see
- * <http://www.gnu.org/licenses/gpl-3.0.html>.
- * #L%
- */
+        /*-
+         * #%L
+         * ProofScriptParser
+         * %%
+         * Copyright (C) 2017 Application-oriented Formal Verification
+         * %%
+         * This program is free software: you can redistribute it and/or modify
+         * it under the terms of the GNU General default License as
+         * published by the Free Software Foundation, either version 3 of the
+         * License, or (at your option) any later version.
+         *
+         * This program is distributed in the hope that it will be useful,
+         * but WITHOUT ANY WARRANTY; without even the implied warranty of
+         * MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE.  See the
+         * GNU General default License for more details.
+         *
+         * You should have received a copy of the GNU General default
+         * License along with this program.  If not, see
+         * <http://www.gnu.org/licenses/gpl-3.0.html>.
+         * #L%
+         */
 
 
 import edu.kit.iti.formal.psdbg.parser.ast.*;
@@ -200,4 +200,30 @@ public interface ASTTraversal<T> extends Visitor<T> {
         func.getArguments().forEach(a -> a.accept(this));
         return null;
     }
+
+    @Override
+    default T visit(WhileStatement ws) {
+        ws.getCondition().accept(this);
+        ws.getBody().accept(this);
+        return null;
+    }
+
+    @Override
+    default T visit(IfStatement is) {
+        is.getCondition().accept(this);
+        is.getBody().accept(this);
+        return null;
+    }
+
+    @Override
+    default T visit(StrictBlock strictBlock) {
+        strictBlock.getBody().accept(this);
+        return null;
+    }
+
+    @Override
+    default T visit(RelaxBlock relaxBlock) {
+        relaxBlock.getBody().accept(this);
+        return null;
+    }
 }

lang/src/main/java/edu/kit/iti/formal/psdbg/parser/DefaultASTVisitor.java

@@ -156,5 +156,25 @@ public class DefaultASTVisitor<T> implements Visitor<T> {
     public T visit(FunctionCall func) {
         return defaultVisit(func);
     }
+
+    @Override
+    public T visit(WhileStatement ws) {
+        return defaultVisit(ws);
+    }
+
+    @Override
+    public T visit(IfStatement is) {
+        return defaultVisit(is);
+    }
+
+    @Override
+    public T visit(StrictBlock strictBlock) {
+        return defaultVisit(strictBlock);
+    }
+
+    @Override
+    public T visit(RelaxBlock relaxBlock) {
+        return defaultVisit(relaxBlock);
+    }
 }
 

lang/src/main/java/edu/kit/iti/formal/psdbg/parser/PrettyPrinter.java

@@ -319,6 +319,51 @@ public class PrettyPrinter extends DefaultASTVisitor<Void> {
         return null;
     }
 
+    @Override
+    public Void visit(DefaultCaseStatement defCase) {
+        return super.visit(defCase);
+    }
+
+    @Override
+    public Void visit(CaseStatement caseStatement) {
+        return super.visit(caseStatement);
+    }
+
+    @Override
+    public Void visit(SubstituteExpression subst) {
+        return super.visit(subst);
+    }
+
+    @Override
+    public Void visit(TryCase TryCase) {
+        return super.visit(TryCase);
+    }
+
+    @Override
+    public Void visit(ClosesCase closesCase) {
+        return super.visit(closesCase);
+    }
+
+    @Override
+    public Void visit(WhileStatement ws) {
+        return super.visit(ws);
+    }
+
+    @Override
+    public Void visit(IfStatement is) {
+        return super.visit(is);
+    }
+
+    @Override
+    public Void visit(StrictBlock strictBlock) {
+        return super.visit(strictBlock);
+    }
+
+    @Override
+    public Void visit(RelaxBlock relaxBlock) {
+        return super.visit(relaxBlock);
+    }
+
     //region Printers little helper
 
     private int getLastNewline() {

lang/src/main/java/edu/kit/iti/formal/psdbg/parser/TransformAst.java

 package edu.kit.iti.formal.psdbg.parser;
 
-/*-
- * #%L
- * ProofScriptParser
- * %%
- * Copyright (C) 2017 Application-oriented Formal Verification
- * %%
- * This program is free software: you can redistribute it and/or modify
- * it under the terms of the GNU General Public License as
- * published by the Free Software Foundation, either version 3 of the
- * License, or (at your option) any later version.
- * 
- * This program is distributed in the hope that it will be useful,
- * but WITHOUT ANY WARRANTY; without even the implied warranty of
- * MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE.  See the
- * GNU General Public License for more details.
- * 
- * You should have received a copy of the GNU General Public
- * License along with this program.  If not, see
- * <http://www.gnu.org/licenses/gpl-3.0.html>.
- * #L%
- */
+        /*-
+         * #%L
+         * ProofScriptParser
+         * %%
+         * Copyright (C) 2017 Application-oriented Formal Verification
+         * %%
+         * This program is free software: you can redistribute it and/or modify
+         * it under the terms of the GNU General Public License as
+         * published by the Free Software Foundation, either version 3 of the
+         * License, or (at your option) any later version.
+         *
+         * This program is distributed in the hope that it will be useful,
+         * but WITHOUT ANY WARRANTY; without even the implied warranty of
+         * MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE.  See the
+         * GNU General Public License for more details.
+         *
+         * You should have received a copy of the GNU General Public
+         * License along with this program.  If not, see
+         * <http://www.gnu.org/licenses/gpl-3.0.html>.
+         * #L%
+         */
 
 
 import edu.kit.iti.formal.psdbg.parser.ast.*;
@@ -39,26 +39,61 @@ import java.util.ArrayList;
 import java.util.LinkedHashMap;
 import java.util.List;
 import java.util.Map;
+import java.util.function.Function;
 import java.util.stream.Collectors;
 
 /**
  * @author Alexander Weigl
  * @version 2 (29.10.17), introduction of parent
- *          version 1 (27.04.17)
+ * version 1 (27.04.17)
  */
 public class TransformAst implements ScriptLanguageVisitor<Object> {
     /**
      * Start index for positional arguments for command calls
      */
     public static final int KEY_START_INDEX_PARAMETER = 2;
+
     @Getter
     private final List<ProofScript> scripts = new ArrayList<>(10);
+
     @Getter
     @Setter
     private FunctionRegister functionRegister = FunctionRegister.getDefault();
 
+    private Function<String, UnconditionalBlock> ubFactory;
+
+    private Function<String, ConditionalBlock> cbFactory;
+
+
     public TransformAst() {
-        //functionRegister.loadDefault();
+        functionRegister.loadDefault();
+        ubFactory = (id -> {
+            switch (id) {
+                case "foreach":
+                    return new ForeachStatement();
+                case "theonly":
+                    return new TheOnlyStatement();
+                case "repeat":
+                    return new RepeatStatement();
+                case "relax":
+                    return new RelaxBlock();
+                case "strict":
+                    return new StrictBlock();
+                default:
+                    throw new RuntimeException("Block " + id + " is not known.");
+            }
+        });
+
+        cbFactory = (id -> {
+            switch (id) {
+                case "if":
+                    return new IfStatement();
+                case "while":
+                    return new WhileStatement();
+                default:
+                    throw new RuntimeException("Block " + id + " is not known.");
+            }
+        });
     }
 
     @Override
@@ -268,11 +303,11 @@ public class TransformAst implements ScriptLanguageVisitor<Object> {
     }
 
     @Override
-    public Map<String, Expression> visitSubstExpressionList(ScriptLanguageParser.SubstExpressionListContext ctx) {
-        Map<String, Expression> map = new LinkedHashMap<>();
+    public Map<String, Expression<ParserRuleContext>> visitSubstExpressionList(ScriptLanguageParser.SubstExpressionListContext ctx) {
+        Map<String, Expression<ParserRuleContext>> map = new LinkedHashMap<>();
         for (int i = 0; i < ctx.scriptVar().size(); i++) {
             map.put(ctx.scriptVar(i).getText(),
-                    (Expression) ctx.expression(i).accept(this));
+                    (Expression<ParserRuleContext>) ctx.expression(i).accept(this));
         }
         return map;
     }
@@ -335,16 +370,6 @@ public class TransformAst implements ScriptLanguageVisitor<Object> {
         throw new IllegalStateException("not implemented");
     }
 
-    @Override
-    public Object visitRepeatStmt(ScriptLanguageParser.RepeatStmtContext ctx) {
-        RepeatStatement rs = new RepeatStatement();
-        rs.setRuleContext(ctx);
-        Statements body = (Statements) ctx.stmtList().accept(this);
-        rs.setBody(body);
-        body.setParent(rs);
-        return rs;
-    }
-
     @Override
     public Object visitCasesStmt(ScriptLanguageParser.CasesStmtContext ctx) {
         CasesStatement cases = new CasesStatement();
@@ -388,25 +413,32 @@ public class TransformAst implements ScriptLanguageVisitor<Object> {
 
 
     @Override
-    public Object visitForEachStmt(ScriptLanguageParser.ForEachStmtContext ctx) {
-        ForeachStatement f = new ForeachStatement();
-        f.setRuleContext(ctx);
+    public UnconditionalBlock visitUnconditionalBlock(ScriptLanguageParser.UnconditionalBlockContext ctx) {
+        List<UnconditionalBlock> list = ctx.kind.stream().map(token -> ubFactory.apply(token.getText())).collect(Collectors.toList());
+        UnconditionalBlock first = list.get(0);
+        UnconditionalBlock last = list.stream().reduce((a, b) -> {
+            b.setParent(a);
+            a.getBody().add(b);
+            return b;
+        }).orElse(first);
+        list.forEach(a -> a.setRuleContext(ctx));
         Statements body = (Statements) ctx.stmtList().accept(this);
-        f.setBody(body);
-        body.setParent(f);
-        return f;
+        last.setBody(body);
+        body.setParent(last);
+        return first;
     }
 
     @Override
-    public Object visitTheOnlyStmt(ScriptLanguageParser.TheOnlyStmtContext ctx) {
-        TheOnlyStatement f = new TheOnlyStatement();
-        f.setRuleContext(ctx);
+    public ConditionalBlock visitConditionalBlock(ScriptLanguageParser.ConditionalBlockContext ctx) {
+        ConditionalBlock cb = cbFactory.apply(ctx.kind.getText());
+        cb.setRuleContext(ctx);
         Statements body = (Statements) ctx.stmtList().accept(this);
-        f.setBody(body);
-        body.setParent(f);
-        return f;
+        cb.setBody(body);
+        body.setParent(cb);
+        return cb;
     }
 
+
     @Override
     public Object visitScriptCommand(ScriptLanguageParser.ScriptCommandContext ctx) {
         CallStatement scs = new CallStatement();

lang/src/main/java/edu/kit/iti/formal/psdbg/parser/Visitor.java

 package edu.kit.iti.formal.psdbg.parser;
 
-/*-
- * #%L
- * ProofScriptParser
- * %%
- * Copyright (C) 2017 Application-oriented Formal Verification
- * %%
- * This program is free software: you can redistribute it and/or modify
- * it under the terms of the GNU General Public License as
- * published by the Free Software Foundation, either version 3 of the
- * License, or (at your option) any later version.
- * 
- * This program is distributed in the hope that it will be useful,
- * but WITHOUT ANY WARRANTY; without even the implied warranty of
- * MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE.  See the
- * GNU General Public License for more details.
- * 
- * You should have received a copy of the GNU General Public
- * License along with this program.  If not, see
- * <http://www.gnu.org/licenses/gpl-3.0.html>.
- * #L%
- */
+        /*-
+         * #%L
+         * ProofScriptParser
+         * %%
+         * Copyright (C) 2017 Application-oriented Formal Verification
+         * %%
+         * This program is free software: you can redistribute it and/or modify
+         * it under the terms of the GNU General Public License as
+         * published by the Free Software Foundation, either version 3 of the
+         * License, or (at your option) any later version.
+         *
+         * This program is distributed in the hope that it will be useful,
+         * but WITHOUT ANY WARRANTY; without even the implied warranty of
+         * MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE.  See the
+         * GNU General Public License for more details.
+         *
+         * You should have received a copy of the GNU General Public
+         * License along with this program.  If not, see
+         * <http://www.gnu.org/licenses/gpl-3.0.html>.
+         * #L%
+         */
 
 import edu.kit.iti.formal.psdbg.parser.ast.*;
 
@@ -81,4 +81,13 @@ public interface Visitor<T> {
     T visit(ClosesCase closesCase);
 
     T visit(FunctionCall func);
+
+    T visit(WhileStatement ws);
+
+    T visit(IfStatement is);
+
+    T visit(StrictBlock strictBlock);
+
+    T visit(RelaxBlock relaxBlock);
+
 }

lang/src/main/java/edu/kit/iti/formal/psdbg/parser/ast/ConditionalBlock.java

+package edu.kit.iti.formal.psdbg.parser.ast;
+
+        /*-
+         * #%L
+         * ProofScriptParser
+         * %%
+         * Copyright (C) 2017 Application-oriented Formal Verification
+         * %%
+         * This program is free software: you can redistribute it and/or modify
+         * it under the terms of the GNU General Public License as
+         * published by the Free Software Foundation, either version 3 of the
+         * License, or (at your option) any later version.
+         *
+         * This program is distributed in the hope that it will be useful,
+         * but WITHOUT ANY WARRANTY; without even the implied warranty of
+         * MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE.  See the
+         * GNU General Public License for more details.
+         *
+         * You should have received a copy of the GNU General Public
+         * License along with this program.  If not, see
+         * <http://www.gnu.org/licenses/gpl-3.0.html>.
+         * #L%
+         */
+
+
+import edu.kit.iti.formal.psdbg.parser.ScriptLanguageParser;
+import lombok.*;
+import org.antlr.v4.runtime.ParserRuleContext;
+
+/**
+ * @author Alexander Weigl
+ * @version 1 (29.04.17)
+ */
+@Getter
+@Setter
+@AllArgsConstructor
+@NoArgsConstructor
+public abstract class ConditionalBlock
+        extends Statement<ScriptLanguageParser.ConditionalBlockContext> {
+    @Getter
+    @Setter
+    @NonNull protected Statements body = new Statements();
+
+    @Getter
+    @Setter
+    @NonNull protected Expression condition = BooleanLiteral.TRUE;
+
+    @Override
+    public boolean eq(ASTNode o) {
+        if (this == o) return true;
+        if (o == null || getClass() != o.getClass()) return false;
+        if (!super.equals(o)) return false;
+
+        ConditionalBlock that = (ConditionalBlock) o;
+
+        return getBody() != null ? getBody().eq(that.getBody()) : that.getBody() == null;
+    }
+
+}

lang/src/main/java/edu/kit/iti/formal/psdbg/parser/ast/ForeachStatement.java

@@ -34,7 +34,7 @@ import lombok.Setter;
  */
 @Getter
 @Setter
-public class ForeachStatement extends GoalSelector<ScriptLanguageParser.ForEachStmtContext> {
+public class ForeachStatement extends UnconditionalBlock {
     public ForeachStatement() {
     }
 

lang/src/main/java/edu/kit/iti/formal/psdbg/parser/ast/GoalSelector.java

-package edu.kit.iti.formal.psdbg.parser.ast;
-
-/*-
- * #%L
- * ProofScriptParser
- * %%
- * Copyright (C) 2017 Application-oriented Formal Verification
- * %%
- * This program is free software: you can redistribute it and/or modify
- * it under the terms of the GNU General Public License as
- * published by the Free Software Foundation, either version 3 of the
- * License, or (at your option) any later version.
- * 
- * This program is distributed in the hope that it will be useful,
- * but WITHOUT ANY WARRANTY; without even the implied warranty of
- * MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE.  See the
- * GNU General Public License for more details.
- * 
- * You should have received a copy of the GNU General Public
- * License along with this program.  If not, see
- * <http://www.gnu.org/licenses/gpl-3.0.html>.
- * #L%
- */
-
-
-
-import lombok.*;
-import org.antlr.v4.runtime.ParserRuleContext;
-
-/**
- * @author Alexander Weigl
- * @version 1 (29.04.17)
- */
-@Getter
-@Setter
-@AllArgsConstructor
-@NoArgsConstructor
-public abstract class GoalSelector<T extends ParserRuleContext>
-        extends Statement<T> {
-    @Getter
-    @Setter
-    @NonNull private Statements body = new Statements();
-
-    @Override
-    public boolean eq(ASTNode o) {
-        if (this == o) return true;
-        if (o == null || getClass() != o.getClass()) return false;
-        if (!super.equals(o)) return false;
-
-        GoalSelector<?> that = (GoalSelector<?>) o;
-
-        return getBody() != null ? getBody().eq(that.getBody()) : that.getBody() == null;
-    }
-
-}

lang/src/main/java/edu/kit/iti/formal/psdbg/parser/ast/IfStatement.java

+package edu.kit.iti.formal.psdbg.parser.ast;
+
+import edu.kit.iti.formal.psdbg.parser.ScriptLanguageParser;
+import edu.kit.iti.formal.psdbg.parser.Visitor;
+
+public class IfStatement extends ConditionalBlock {
+    @Override
+    public <T> T accept(Visitor<T> visitor) {
+        return visitor.visit(this);
+    }
+
+    @Override
+    public Statement<ScriptLanguageParser.ConditionalBlockContext> copy() {
+        IfStatement is = new IfStatement();
+        is.ruleContext = ruleContext;
+        is.body = body.copy();
+        is.condition = condition.copy();
+        return is;
+    }
+}

lang/src/main/java/edu/kit/iti/formal/psdbg/parser/ast/RelaxBlock.java

+package edu.kit.iti.formal.psdbg.parser.ast;
+
+import edu.kit.iti.formal.psdbg.parser.Visitor;
+
+public class RelaxBlock extends UnconditionalBlock {
+    @Override
+    public <T> T accept(Visitor<T> visitor) {
+        return visitor.visit(this);
+    }
+
+    @Override
+    public RelaxBlock copy() {
+        RelaxBlock sb = new RelaxBlock();
+        sb.body = body.copy();
+        sb.ruleContext = ruleContext;
+        return sb;
+    }
+}

lang/src/main/java/edu/kit/iti/formal/psdbg/parser/ast/RepeatStatement.java

@@ -34,7 +34,7 @@ import lombok.Setter;
  */
 @Getter
 @Setter
-public class RepeatStatement extends GoalSelector<ScriptLanguageParser.RepeatStmtContext> {
+public class RepeatStatement extends UnconditionalBlock {
     public RepeatStatement() {
     }
 
@@ -59,6 +59,4 @@ public class RepeatStatement extends GoalSelector<ScriptLanguageParser.RepeatStm
         rs.setRuleContext(this.ruleContext);
         return rs;
     }
-
-
 }

lang/src/main/java/edu/kit/iti/formal/psdbg/parser/ast/StrictBlock.java

+package edu.kit.iti.formal.psdbg.parser.ast;
+
+import edu.kit.iti.formal.psdbg.parser.Visitor;
+
+public class StrictBlock extends UnconditionalBlock {
+    @Override
+    public <T> T accept(Visitor<T> visitor) {
+        return visitor.visit(this);
+    }
+
+    @Override
+    public StrictBlock copy() {
+        StrictBlock sb = new StrictBlock();
+        sb.body = body.copy();
+        sb.ruleContext = ruleContext;
+        return sb;
+    }
+}

lang/src/main/java/edu/kit/iti/formal/psdbg/parser/ast/TheOnlyStatement.java

@@ -34,7 +34,7 @@ import lombok.Setter;
  */
 @Getter
 @Setter
-public class TheOnlyStatement extends GoalSelector<ScriptLanguageParser.TheOnlyStmtContext> {
+public class TheOnlyStatement extends UnconditionalBlock {
     public TheOnlyStatement() {
     }
 

lang/src/main/java/edu/kit/iti/formal/psdbg/parser/ast/UnconditionalBlock.java

+package edu.kit.iti.formal.psdbg.parser.ast;
+
+        /*-
+         * #%L
+         * ProofScriptParser
+         * %%
+         * Copyright (C) 2017 Application-oriented Formal Verification
+         * %%
+         * This program is free software: you can redistribute it and/or modify
+         * it under the terms of the GNU General Public License as