From e140d6faee6977640466f2a8db8b588bfc1a3dde Mon Sep 17 00:00:00 2001
From: hansen <dominik_hansen@web.de>
Date: Mon, 10 Nov 2014 16:01:19 +0100
Subject: [PATCH] parse LTL formulas only when it is necessary
---
src/main/java/de/tlc4b/analysis/MachineContext.java | 11 +++++++----
1 file changed, 7 insertions(+), 4 deletions(-)
diff --git a/src/main/java/de/tlc4b/analysis/MachineContext.java b/src/main/java/de/tlc4b/analysis/MachineContext.java
index aa242f5..90cc278 100644
--- a/src/main/java/de/tlc4b/analysis/MachineContext.java
+++ b/src/main/java/de/tlc4b/analysis/MachineContext.java
@@ -68,6 +68,7 @@ import de.be4.classicalb.core.parser.node.PPredicate;
import de.be4.classicalb.core.parser.node.PSet;
import de.be4.classicalb.core.parser.node.Start;
import de.be4.classicalb.core.parser.node.TIdentifierLiteral;
+import de.tlc4b.TLC4BGlobals;
import de.tlc4b.exceptions.ScopeException;
import de.tlc4b.ltl.LTLBPredicate;
import de.tlc4b.ltl.LTLFormulaVisitor;
@@ -297,10 +298,12 @@ public class MachineContext extends DepthFirstAdapter {
AExpressionDefinitionDefinition def = (AExpressionDefinitionDefinition) e;
String name = def.getName().getText();
if (name.startsWith("ASSERT_LTL")) {
- LTLFormulaVisitor visitor = new LTLFormulaVisitor(name, this);
- visitor.parseDefinition(def);
- this.ltlVisitors.add(visitor);
-
+ if (TLC4BGlobals.isCheckltl()) {
+ LTLFormulaVisitor visitor = new LTLFormulaVisitor(name,
+ this);
+ visitor.parseDefinition(def);
+ this.ltlVisitors.add(visitor);
+ }
definitionsToRemove.add(def);
} else if (name.startsWith("ANIMATION_")) {
definitionsToRemove.add(def);
--
GitLab