Skip to content
Snippets Groups Projects
Commit f00b364e authored by Michael Leuschel's avatar Michael Leuschel
Browse files

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: default avatarMichael Leuschel <leuschel@uni-duesseldorf.de>
parent a0cd2ca9
No related branches found
No related tags found
No related merge requests found
Pipeline #156246 passed
...@@ -1240,6 +1240,12 @@ private static class ModelChecker { ...@@ -1240,6 +1240,12 @@ private static class ModelChecker {
this.isDebug = isDebug; this.isDebug = isDebug;
} }
void debug_println (String msg) {
if(isDebug) {
System.out.println(msg);
}
}
<main> <main>
private <machine> next() { private <machine> next() {
...@@ -1514,8 +1520,8 @@ while(!currentState._get_calculate_flag_cp()) { ...@@ -1514,8 +1520,8 @@ while(!currentState._get_calculate_flag_cp()) {
<machine> copiedState = state._copy(); <machine> copiedState = state._copy();
copiedState._apply_<operation>_cp(currentState); copiedState._apply_<operation>_cp(currentState);
copiedState.<operation>(<parameters; separator=", ">); copiedState.<operation>(<parameters; separator=", ">);
<if(isCaching)>
copiedState.parent = state; copiedState.parent = state;
<if(isCaching)>
copiedState = stateAccessedVia = "<operation>(<parameters; separator=", ">)"; copiedState = stateAccessedVia = "<operation>(<parameters; separator=", ">)";
<endif> <endif>
if(copiedState._get_<operation>_triggered()) { if(copiedState._get_<operation>_triggered()) {
...@@ -1563,6 +1569,7 @@ try { ...@@ -1563,6 +1569,7 @@ try {
} }
<else> <else>
copiedState.<operation>(<parameters; separator=", ">); copiedState.<operation>(<parameters; separator=", ">);
copiedState.parent = state;
<endif> <endif>
result.add(copiedState); result.add(copiedState);
transitions.getAndIncrement(); transitions.getAndIncrement();
...@@ -1598,6 +1605,7 @@ if(_OpCache_with_parameter_<operation> != null) { ...@@ -1598,6 +1605,7 @@ if(_OpCache_with_parameter_<operation> != null) {
} }
<else> <else>
copiedState.<operation>(<parameters; separator=", ">); copiedState.<operation>(<parameters; separator=", ">);
copiedState.parent = state;
<endif> <endif>
result.add(copiedState); result.add(copiedState);
transitions.getAndIncrement(); transitions.getAndIncrement();
...@@ -1669,7 +1677,7 @@ private void printResult(final int states, final int transitions) { ...@@ -1669,7 +1677,7 @@ private void printResult(final int states, final int transitions) {
if(counterExampleState.stateAccessedVia != null) { if(counterExampleState.stateAccessedVia != null) {
sb.insert(0, counterExampleState.stateAccessedVia); sb.insert(0, counterExampleState.stateAccessedVia);
} }
sb.insert(0, "\n" + "* Step " + stepnr + ":"); sb.insert(0, "\n" + "* Step: ");
stepnr++; stepnr++;
counterExampleState = counterExampleState.parent; counterExampleState = counterExampleState.parent;
} }
...@@ -1689,14 +1697,12 @@ model_check_init_static(map, keyy, entries) ::= << ...@@ -1689,14 +1697,12 @@ model_check_init_static(map, keyy, entries) ::= <<
model_check_main(machine, invariants, invariantDependency, guardDependency) ::= << model_check_main(machine, invariants, invariantDependency, guardDependency) ::= <<
public void modelCheck() { public void modelCheck() {
if (isDebug) {
System.out.println("Starting Modelchecking, STRATEGY=" + type + ", THREADS=" + threads + ", CACHING=" + isCaching);
}
if (threads \<= 1) { if (threads \<= 1) {
debug_println("Starting Single-Threaded Modelchecking, STRATEGY=" + type + ", THREADS=" + threads + ", CACHING=" + isCaching);
modelCheckSingleThreaded(); modelCheckSingleThreaded();
} else { } else {
debug_println("Starting Multi-Threaded Modelchecking, STRATEGY=" + type + ", THREADS=" + threads + ", CACHING=" + isCaching);
this.threadPool = (ThreadPoolExecutor) Executors.newFixedThreadPool(threads-1); this.threadPool = (ThreadPoolExecutor) Executors.newFixedThreadPool(threads-1);
modelCheckMultiThreaded(); modelCheckMultiThreaded();
} }
......
0% Loading or .
You are about to add 0 people to the discussion. Proceed with caution.
Please register or to comment