From f00b364e1acbf697dc10c689160f80e7be435ad3 Mon Sep 17 00:00:00 2001
From: Michael Leuschel <leuschel@uni-duesseldorf.de>
Date: Wed, 28 May 2025 10:55:24 +0200
Subject: [PATCH] fix counter example computation/display
in Java for non-caching mode
(the use of the string builder to display the counter example
is still a bit ugly and should include the step number,
for non-caching mode also the name of the transition
is not displayed, probably because it is not stored)
Signed-off-by: Michael Leuschel <leuschel@uni-duesseldorf.de>
---
.../hhu/stups/codegenerator/JavaTemplate.stg | 18 ++++++++++++------
1 file changed, 12 insertions(+), 6 deletions(-)
diff --git a/src/main/resources/de/hhu/stups/codegenerator/JavaTemplate.stg b/src/main/resources/de/hhu/stups/codegenerator/JavaTemplate.stg
index f2c2a414..42d27bb3 100644
--- a/src/main/resources/de/hhu/stups/codegenerator/JavaTemplate.stg
+++ b/src/main/resources/de/hhu/stups/codegenerator/JavaTemplate.stg
@@ -1239,6 +1239,12 @@ private static class ModelChecker {
this.isCaching = isCaching;
this.isDebug = isDebug;
}
+
+ void debug_println (String msg) {
+ if(isDebug) {
+ System.out.println(msg);
+ }
+ }
<main>
@@ -1514,8 +1520,8 @@ while(!currentState._get_calculate_flag_cp()) {
<machine> copiedState = state._copy();
copiedState._apply_<operation>_cp(currentState);
copiedState.<operation>(<parameters; separator=", ">);
- <if(isCaching)>
copiedState.parent = state;
+ <if(isCaching)>
copiedState = stateAccessedVia = "<operation>(<parameters; separator=", ">)";
<endif>
if(copiedState._get_<operation>_triggered()) {
@@ -1563,6 +1569,7 @@ try {
}
<else>
copiedState.<operation>(<parameters; separator=", ">);
+ copiedState.parent = state;
<endif>
result.add(copiedState);
transitions.getAndIncrement();
@@ -1598,6 +1605,7 @@ if(_OpCache_with_parameter_<operation> != null) {
}
<else>
copiedState.<operation>(<parameters; separator=", ">);
+copiedState.parent = state;
<endif>
result.add(copiedState);
transitions.getAndIncrement();
@@ -1669,7 +1677,7 @@ private void printResult(final int states, final int transitions) {
if(counterExampleState.stateAccessedVia != null) {
sb.insert(0, counterExampleState.stateAccessedVia);
}
- sb.insert(0, "\n" + "* Step " + stepnr + ":");
+ sb.insert(0, "\n" + "* Step: ");
stepnr++;
counterExampleState = counterExampleState.parent;
}
@@ -1689,14 +1697,12 @@ model_check_init_static(map, keyy, entries) ::= <<
model_check_main(machine, invariants, invariantDependency, guardDependency) ::= <<
public void modelCheck() {
- if (isDebug) {
- System.out.println("Starting Modelchecking, STRATEGY=" + type + ", THREADS=" + threads + ", CACHING=" + isCaching);
- }
if (threads \<= 1) {
-
+ debug_println("Starting Single-Threaded Modelchecking, STRATEGY=" + type + ", THREADS=" + threads + ", CACHING=" + isCaching);
modelCheckSingleThreaded();
} else {
+ debug_println("Starting Multi-Threaded Modelchecking, STRATEGY=" + type + ", THREADS=" + threads + ", CACHING=" + isCaching);
this.threadPool = (ThreadPoolExecutor) Executors.newFixedThreadPool(threads-1);
modelCheckMultiThreaded();
}
--
GitLab