Skip to content
New issue

Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.

Sign up for GitHub

By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.

Already on GitHub? Sign in to your account

Wrong k-bound passed when using approximation with raw verification - fix 2052379 #135

Merged
merged 11 commits into from
Feb 12, 2024
Merged

Wrong k-bound passed when using approximation with raw verification - fix 2052379 #135

Show file tree
Hide file tree
Changes from 1 commit
Commits
Show all changes
11 commits
Select commit Hold shift + click to select a range
d3eb8ac
Fixed wrong k-bound passed when using approximation with raw verifica…
mtygesen Feb 4, 2024
fc7528d
If using approximation with raw verification it will now ignore the -…
mtygesen Feb 5, 2024
47b1e19
Added warning that k-bound will be overwritten
mtygesen Feb 6, 2024
f5ebf0b
Remove unused import
mtygesen Feb 6, 2024
8cd8817
Fixed k-bound not updating, and fixed exception thrown by loadDocumen…
mtygesen Feb 7, 2024
e700607
Fixed issue with --k-bound duplicating
mtygesen Feb 8, 2024
9dc7202
Raw verification options now overwrite --trace as well
mtygesen Feb 11, 2024
48b10ef
Update branch to state of main
mtygesen Feb 11, 2024
dc12018
Fixed issue that would cause problems showing traces in certain cases
mtygesen Feb 11, 2024
ca52346
Removed debug logging
mtygesen Feb 11, 2024
d34bd38
Fixed NPE when trying to add bindings to net that should not be unfolded
mtygesen Feb 12, 2024
File filter

Filter by extension

Filter by extension
Conversations
Failed to load comments.
Loading
Jump to
Jump to file
Failed to load files.
Loading
Diff view
Diff view
3 changes: 3 additions & 0 deletions src/main/java/dk/aau/cs/verification/VerifyTAPN/VerifyDTAPNOptions.java
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -103,6 +103,9 @@ public String toString() {
StringBuilder result = new StringBuilder();

if (useRawVerification) {
if (rawVerificationOptions != null) {
rawVerificationOptions = rawVerificationOptions.replaceAll("(--k-bound|-k) +\\d+", "$1 " + kBound());
}
return result.append(rawVerificationOptions).toString();
}

Expand Down
6 changes: 4 additions & 2 deletions src/main/java/dk/aau/cs/verification/VerifyTAPN/VerifyPNOptions.java
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -184,11 +184,13 @@ public String toString() {
StringBuilder result = new StringBuilder();

if (useRawVerification) {
if (rawVerificationOptions != null) {
rawVerificationOptions = rawVerificationOptions.replaceAll("(--k-bound|-k) +\\d+", "$1 " + kBound());
}
return result.append(rawVerificationOptions).toString();
}

result.append("--k-bound ");
result.append(extraTokens+tokensInModel);
result.append(kBoundArg());

var traceSwitch =traceMap.get(traceOption) ;
if (traceSwitch != null) {
Expand Down
9 changes: 8 additions & 1 deletion src/main/java/dk/aau/cs/verification/VerifyTAPN/VerifyTAPNOptions.java
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -88,9 +88,13 @@ public void setTokensInModel(int tokens){ // TODO: Get rid of this method when v
}

public String kBoundArg() {
return " --k-bound " + (extraTokens+tokensInModel) + " ";
return "--k-bound " + kBound() + " ";
}

public int kBound() {
return (extraTokens + tokensInModel);
}

public String deadTokenArg() {
return dontUseDeadPlaces ? " --keep-dead-tokens " : "";
}
Expand All @@ -100,6 +104,9 @@ public String toString() {
StringBuilder result = new StringBuilder();

if (useRawVerification) {
if (rawVerificationOptions != null) {
rawVerificationOptions = rawVerificationOptions.replaceAll("(--k-bound|-k) +\\d+", "$1 " + kBound());
}
return result.append(rawVerificationOptions).toString();
}

Expand Down
Loading