-
Notifications
You must be signed in to change notification settings - Fork 5
McNet : CTL Model Checking #153
Copy link
Copy link
Open
Labels
help wantedExtra attention is neededExtra attention is needed⏰ benchmarkNew or changes to existing benchmarkNew or changes to existing benchmark🎓 student projectInteresting (~ 5 ECTS) side projectsInteresting (~ 5 ECTS) side projects
Milestone
Description
Metadata
Metadata
Assignees
Labels
help wantedExtra attention is neededExtra attention is needed⏰ benchmarkNew or changes to existing benchmarkNew or changes to existing benchmark🎓 student projectInteresting (~ 5 ECTS) side projectsInteresting (~ 5 ECTS) side projects
The McNet benchmark has already includes most of the pieces for CTL model checking. We can repurpose the expression parser to take in a formula given as a command line argument. Then, we can implement the solver by executing the respective fixpoint algorithms on a stack-evaluation of the formula.