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

Jump to bottom

Wip/lf/pea complement only #670

Merged
merged 120 commits into from
Aug 14, 2024
Merged

Wip/lf/pea complement only #670

merged 120 commits into from
Aug 14, 2024

Conversation

henkele
Copy link
Contributor

@henkele henkele commented Aug 9, 2024

Implements PEA complement and redundancy analysis

lf274 added 30 commits August 8, 2024 17:06
@lf274 @henkele
started implementing algorithm for pea complementation
b9f53a8
@lf274 @henkele
small bugfixes
46ca2c1
@lf274 @henkele
small bugfixes. algorithm runs now without errors, nice
3e8de86
@lf274 @henkele
improved strict() and noReset() methods
7ab2edc
@lf274 @henkele
tried different things for noReset(), RangeDecision.py: in methodss g…
c2a5b3e 
…etOP and getVal, renamed argument from "childs" to "trueChildIndex"
@lf274 @henkele
started implementing filterCdd() and strict() in RangeDecision class
744b847
@lf274 @henkele
Added test RangeDecisionTest to test my implementation of filterCdd()…
87f7632 
… and strict()
@lf274 @henkele
implemented getDecisions() in Class CDD, implemented Test cases, fixe…
417545e 
…d bugs
@lf274 @henkele
work in progress, added useful pair class
cdc0013
@lf274 @henkele
added SimplePair class
2dcf01e
@lf274 @henkele
implemented unit tests, bugfixing, started adding documentation
73cf081
@lf274 @henkele
more test cases, test file documentation
11db31c
@lf274 @henkele
Put my tests in newly created class CddUnitTest, as to leave CddTest …
d83a58c 
…as it was
@lf274 @henkele
implemented strict() in class RangeDecision
d726ec8
@lf274 @henkele
changed getDecisionConjunction to be iterative and simpler. Tested it…
05976ce 
…. Removed unnecessary SimplePair class, now my implementation uses Pair class that was already there
@lf274 @henkele
removed old import
9d38dff
@lf274 @henkele
added tests for strict(), fixed bugs
4a8fa32
@lf274 @henkele
added class for initial transitions: InitialTransisition
85401ba
@lf274 @henkele
added optional member mInitialTransition in class Phase, removed unne…
6b1ab1d 
…cessary method in RangeDecision Class
@lf274 @henkele
initial transistions are now being added in method parallel() of clas…
6e72546 
…s PhaseEventAutomata
@lf274 @henkele
changed complementation algorithm to use new implementations of filte…
f6a30fb 
…rCdd and strict
@lf274 @henkele
cleaned up test class CddUnitTest, added initial edge for sink comput…
c148ba7 
…ation in ComplementPea
@lf274 @henkele
fixed bugs in ComplementPea and PhaseEventAutomaton
344d6db
@lf274 @henkele
more tests, bugfixing
3a481ff
@lf274 @henkele
startet implementing check for emptiness of intersection of PEAs
0d13c03
@lf274 @henkele
finished implementing intersection emptiness check
782826d
@lf274 @henkele
added another test (special case example: DurationBoundUGlobally
39cd627
@lf274 @henkele
small changes to test
ae8ec6b
@lf274 @henkele
implemented check for complement: annotations, preferences, check gen…
af3727f 
…eration and assertion generation
@lf274 @henkele
fixed documentation
bb123e4
@danieldietsch
Copy link
Member

@henkele @Langenfeld I fixed the various CC issues in 1a1883a. From my side, only the issues with CDD.getDecisionsConjunction() remain.

@danieldietsch
Copy link
Member

Oh, and I just realized: not all new files have copyright headers. Could you check for

A       trunk/source/Library-PEA/src/de/uni_freiburg/informatik/ultimate/lib/pea/InitialTransition.java
A       trunk/source/Library-PEA/src/de/uni_freiburg/informatik/ultimate/lib/pea/PEAComplement.java
A       trunk/source/Library-PEATest/src/de/uni_freiburg/informatik/ultimate/lib/pea/test/CddUnitTest.java
A       trunk/source/Library-PEATest/src/de/uni_freiburg/informatik/ultimate/lib/pea/test/ComplementPEATest.java
A       trunk/source/Library-PEATest/src/de/uni_freiburg/informatik/ultimate/lib/pea/test/RangeDecisionTest.java
A       trunk/source/PEAtoBoogie/src/de/uni_freiburg/informatik/ultimate/pea2boogie/translator/RedundancyTransformer.java
A       trunk/source/PEAtoBoogie/src/de/uni_freiburg/informatik/ultimate/pea2boogie/translator/RedundancyTransformerReq2Pea.java
A       trunk/source/UltimateRegressionTest/src/de/uni_freiburg/informatik/ultimate/regressiontest/generic/ReqCheckerRedundancyRegressionTestSuite.java

@henkele
test: add new testcases for redundancy
b6f0327
@henkele
style: add missing copyright headers
6c77b8f
@henkele
refactor: modify strict PEAs before computing the guards to the sink …
9ebd21e 
…transition as this simplifies the computation of the sink guard (source clock invariant not needed anymore, as non-modified clock is now explicitly in the guard of the outgoing transition)
@henkele
docs: add comment and todo
71c0b0b
@henkele
test: more/modified regression tests
8a10bf6
@danieldietsch danieldietsch merged commit b7ce1da into dev Aug 14, 2024
2 checks passed
@danieldietsch danieldietsch deleted the wip/lf/pea-complement-only branch August 14, 2024 15:23
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment
Reviewers

@maul-esel maul-esel maul-esel left review comments

@Langenfeld Langenfeld Awaiting requested review from Langenfeld

@danieldietsch danieldietsch Awaiting requested review from danieldietsch

Assignees
No one assigned
Labels
feature ReqAnalyzer
Projects
None yet
Milestone
No milestone
Development

Successfully merging this pull request may close these issues.
6 participants
@henkele @danieldietsch @bahnwaerter @maul-esel @Langenfeld @lf274