Ticket #519 (new task)
Connect Hets to SMV model checker (full integration)
| Reported by: | till | Owned by: | hartke |
|---|---|---|---|
| Priority: | critical | Milestone: | 0.95 |
| Component: | provers | Version: | 0.8 |
| Keywords: | Cc: |
Description (last modified by till) (diff)
- write parser for temporal logic syntax
- write abstract syntax, parser and printer for muSMV model syntax
- write an instance for logic Temporal of type class Logic (see source:trunk/Logic/Logic.hs, see source:trunk/Propositional/Logic_Propositional.hs)
- integrate muSMV as a prover in Hets (see source:trunk/Logic/Prover.hs)
first complete #518
Change History
Note: See
TracTickets for help on using
tickets.