TAPAAL

Merge lp:~tapaal-contributor/tapaal/broken-boundedness-check-games-2006111 into lp:tapaal/3.9

  1. broken-boundedness-check-games-2006111
  2. Merge into 3.9
Proposed by Lena Ernstsen
Status: Merged
Approved by: Jiri Srba
Approved revision: 1181
Merged at revision: 1180
Proposed branch: lp:~tapaal-contributor/tapaal/broken-boundedness-check-games-2006111
Merge into: lp:tapaal/3.9
Diff against target: 59 lines (+12/-8)
3 files modified
src/dk/aau/cs/verification/VerificationResult.java (+8/-6)
src/dk/aau/cs/verification/VerifyTAPN/VerifyDTAPNOptions.java (+2/-1)
src/pipe/gui/KBoundAnalyzer.java (+2/-1)
To merge this branch: bzr merge lp:~tapaal-contributor/tapaal/broken-boundedness-check-games-2006111
Reviewer Review Type Date Requested Status
Jiri Srba Approve
Review via email: mp+436900@code.launchpad.net

Commit message

Fixed boundedness check error for game nets

To post a comment you must log in.
Revision history for this message
Jiri Srba (srba) :
review: Approve

Preview Diff

[H/L] Next/Prev Comment, [J/K] Next/Prev File, [N/P] Next/Prev Hunk
1=== modified file 'src/dk/aau/cs/verification/VerificationResult.java'
2--- src/dk/aau/cs/verification/VerificationResult.java 2023-01-09 11:11:07 +0000
3+++ src/dk/aau/cs/verification/VerificationResult.java 2023-02-06 11:17:40 +0000
4@@ -36,12 +36,14 @@
5 this.stats = stats;
6 this.rawOutput = rawOutput;
7
8- String[] lines = rawOutput.split(System.getProperty("line.separator"));
9- for (String line : lines) {
10- Matcher matcher = Pattern.compile("\\s*-k\\s*(\\d+)\\s*").matcher(line);
11- if (matcher.find()) {
12- this.bound = Integer.parseInt(matcher.group(1));
13- break;
14+ if (rawOutput != null) {
15+ String[] lines = rawOutput.split(System.getProperty("line.separator"));
16+ for (String line : lines) {
17+ Matcher matcher = Pattern.compile("\\s*-k\\s*(\\d+)\\s*").matcher(line);
18+ if (matcher.find()) {
19+ this.bound = Integer.parseInt(matcher.group(1));
20+ break;
21+ }
22 }
23 }
24 }
25
26=== modified file 'src/dk/aau/cs/verification/VerifyTAPN/VerifyDTAPNOptions.java'
27--- src/dk/aau/cs/verification/VerifyTAPN/VerifyDTAPNOptions.java 2020-07-13 13:58:47 +0000
28+++ src/dk/aau/cs/verification/VerifyTAPN/VerifyDTAPNOptions.java 2023-02-06 11:17:40 +0000
29@@ -23,6 +23,7 @@
30 TraceOption traceOption,
31 SearchOption search,
32 boolean symmetry,
33+ boolean gcd,
34 boolean timeDarts,
35 boolean pTrie,
36 boolean enableOverApproximation,
37@@ -30,7 +31,7 @@
38 int approximationDenominator,
39 boolean stubbornReduction
40 ) {
41- this(extraTokens, traceOption, search, symmetry, true, timeDarts, pTrie, false, false, new InclusionPlaces(), WorkflowMode.NOT_WORKFLOW, 0, enableOverApproximation, enableUnderApproximation, approximationDenominator, stubbornReduction);
42+ this(extraTokens, traceOption, search, symmetry, gcd, timeDarts, pTrie, false, false, new InclusionPlaces(), WorkflowMode.NOT_WORKFLOW, 0, enableOverApproximation, enableUnderApproximation, approximationDenominator, stubbornReduction);
43 this.dontUseDeadPlaces = dontUseDeadPlaces;
44 }
45
46
47=== modified file 'src/pipe/gui/KBoundAnalyzer.java'
48--- src/pipe/gui/KBoundAnalyzer.java 2021-10-02 16:01:49 +0000
49+++ src/pipe/gui/KBoundAnalyzer.java 2023-02-06 11:17:40 +0000
50@@ -71,7 +71,8 @@
51 } else if(modelChecker instanceof VerifyTAPN){
52 return new VerifyTAPNOptions(k, TraceOption.NONE, SearchOption.BFS, true, false, true, false, false, 1);
53 } else if(modelChecker instanceof VerifyTAPNDiscreteVerification){
54- return new VerifyDTAPNOptions(true, k, TraceOption.NONE, SearchOption.BFS, true, !tapnNetwork.hasUrgentTransitions(), true, false, false, 1, false);
55+ boolean isGame = CreateGui.getCurrentTab().getLens().isGame();
56+ return new VerifyDTAPNOptions(true, k, TraceOption.NONE, SearchOption.BFS, true, !isGame, !tapnNetwork.hasUrgentTransitions(), true, false, false, 1, false);
57 }
58 return null;
59 }

Subscribers

People subscribed via source and target branches