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

DFS verification expansion #35

Closed
wants to merge 20 commits into from
Closed

DFS verification expansion #35

wants to merge 20 commits into from

Conversation

acepace
Copy link
Contributor

@acepace acepace commented Apr 10, 2018 •
edited
Loading

  • Added the concept of invalid events to the DFS verifier (enables testing for persistence properties).
  • Expanded the DFS Verifier test suite
  • Fixed bugs in DiningPhilosophers tests
  • Added tests for bp.assert in both BProgram and the DFS verifier
  • Generic code cleanup using IntelliJ code analyser

Ace Pace and others added 18 commits March 12, 2018 15:09
Allow using let statements in bpjs programs.
6a340e9
Move to using let in BPJSDiningPhil.js
f9050a7 
Change eventSet to event in addStick
Fix what we're blocking in addStick second bsync
Check for O wins or draws.
123bf97
Add new verification result, badState, to cover when we reach an inva…
9e57452 
…lid situation
Add new type of test, have we visited a state we don't want to reach.
39dc326 
Made TicTacToeGame use it to see that our strategy is a failure and a draw can occur.
Fix documentation bug
9cfefe3
Remove boolean flag on detecting invalid states
15f0720
@geraw
.
07d1a30
@geraw
Currently broken test in DfsBProgramVerifierTest
99d9601
Move some code around.
5bdd0a4 
IntelliJ code formatter run
Fix bug in test for Java variables
6517e6f
Create concept of VerificationResult keeping the invalid state and no…
9a7caf5 
…t just the flag. Update call locations to account for it.
Create tests for invalid states
98b543c
Add test for invalid events + deadlock setting
30b5d4f
Some more settings tests, for better coverage
1b40775
Add test for assert right at start of execution of a bThread
0e08890
Generic code cleanup using IntelliJ code analyser.
16a2cc4
#2 Generic code cleanup using IntelliJ code analyser.
f343fb4
@acepace acepace closed this Apr 10, 2018
@acepace acepace reopened this Apr 10, 2018
@coveralls
Copy link

Coverage Status

Coverage increased (+1.8%) to 82.229% when pulling 1e57cf5 on acepace:develop into f02f1fa on bThink-BGU:develop.

@acepace acepace changed the title Rebase DFS verification expansion Apr 16, 2018
@acepace acepace closed this Apr 20, 2018
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment
Reviewers
No reviews
Assignees
No one assigned
Labels
None yet
Projects
None yet
Milestone
No milestone
Development

Successfully merging this pull request may close these issues.

None yet
3 participants
@acepace @coveralls @geraw