From 2c59e5b6264448d334bad0966d07b3bb29d4087a Mon Sep 17 00:00:00 2001
From: Michael Leuschel <leuschel@uni-duesseldorf.de>
Date: Fri, 11 Jun 2021 14:48:56 +0200
Subject: [PATCH] disalbe safety model checking by default

the generated counter examples are not in
the right format for the ProB for Rodin plugin
---
 de.prob.core/src/de/prob/cli/CliStarter.java | 3 +++
 1 file changed, 3 insertions(+)

diff --git a/de.prob.core/src/de/prob/cli/CliStarter.java b/de.prob.core/src/de/prob/cli/CliStarter.java
index 3e1dcb21..f160beec 100644
--- a/de.prob.core/src/de/prob/cli/CliStarter.java
+++ b/de.prob.core/src/de/prob/cli/CliStarter.java
@@ -85,6 +85,9 @@ public final class CliStarter {
 		// command.add("-ll");
 		command.add("-sf");
 		command.add("-parsercp");
+		command.add("-p");command.add("use_safety_ltl_model_checker");command.add("false");
+		 // disable LTL safety model check as the counter examples lead to assertion failures 
+		 // in CounterExampleProposition in CounterExample.java
 		command.add(fullcp);
 
 		if (file != null) {
-- 
GitLab