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.

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

Add support for new property check for requirements called State-Recoverability #645

Open
wants to merge 24 commits into
base: dev
Choose a base branch
from
Open
Changes from 1 commit
Commits
Show all changes
24 commits
Select commit Hold shift + click to select a range
33d9103
Add support for new property check for requirements called
Tob1as864 Aug 15, 2023
6c8af66
Update trunk/source/Library-UltimateModel/src/de/uni_freiburg/informa…
Tob1as864 Aug 15, 2023
3de1715
Update trunk/source/PEAtoBoogie/src/de/uni_freiburg/informatik/ultima…
Tob1as864 Aug 15, 2023
b531f42
Update trunk/source/PEAtoBoogie/src/de/uni_freiburg/informatik/ultima…
Tob1as864 Aug 15, 2023
b4aa9f5
Update trunk/source/PEAtoBoogie/src/de/uni_freiburg/informatik/ultima…
Tob1as864 Aug 15, 2023
3096f1e
Update trunk/source/PEAtoBoogie/src/de/uni_freiburg/informatik/ultima…
Tob1as864 Aug 15, 2023
9d4e8be
Update trunk/source/PEAtoBoogie/src/de/uni_freiburg/informatik/ultima…
Tob1as864 Aug 15, 2023
3ed0ed0
Update trunk/source/PEAtoBoogie/src/de/uni_freiburg/informatik/ultima…
Tob1as864 Aug 15, 2023
39b357f
Update trunk/source/PEAtoBoogie/src/de/uni_freiburg/informatik/ultima…
Tob1as864 Aug 15, 2023
177838a
Fixes for pull request
Tob1as864 Aug 15, 2023
ba1afa3
Merge remote-tracking branch 'origin/NewPropertyForRequirementsCheck'
Tob1as864 Aug 15, 2023
a485799
Fixes for review
Tob1as864 Aug 15, 2023
3eac26a
Review fix
Tob1as864 Aug 28, 2023
76c1170
Review fix
Tob1as864 Aug 28, 2023
d9cf93c
Review fix
Tob1as864 Aug 28, 2023
661a8b7
Review fix
Tob1as864 Aug 29, 2023
503cb86
Bugfix
Tob1as864 Aug 29, 2023
bb7fa8e
Bugfix
Tob1as864 Aug 30, 2023
d6637ba
Removed import
Tob1as864 Aug 30, 2023
6c6b86a
Verification Condition as Expression
Tob1as864 Aug 31, 2023
a767340
Review fix
Tob1as864 Aug 31, 2023
b55702b
Bugfix for property check without any assertations
Tob1as864 Sep 3, 2023
f09372a
Bugfix
Tob1as864 Sep 23, 2023
7d75049
Resolve Boogie data type issue
Tob1as864 Nov 21, 2023
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
Prev Previous commit
Next Next commit
Fixes for review
  • Loading branch information
Tob1as864 committed Aug 15, 2023
commit a4857995b61e4589eccde012bf19d945f6a551c8
Original file line number Diff line number Diff line change
@@ -219,6 +219,7 @@ private List<Statement> genCheckStateRecoverability(final BoogieLocation bl) {
}

// DOT printen
/*
final List<Entry<PatternType<?>, PhaseEventAutomata>> counterTracePEAList = new ArrayList<>();
for (final ReqPeas reqPea : mReqPeas) {
final PatternType<?> pattern = reqPea.getPattern();
@@ -229,8 +230,8 @@ private List<Statement> genCheckStateRecoverability(final BoogieLocation bl) {
}
final List<Entry<PatternType<?>, PhaseEventAutomata>[]> subsets = CrossProducts.subArrays(counterTracePEAList.toArray(new Entry[counterTracePEAList.size()]), counterTracePEAList.size(), new Entry[counterTracePEAList.size()]);
//Prints parallel automaton
//dotPrinter(subsets);

dotPrinter(subsets);
*/
return list;
}