Ticket #518 (new task)

Opened 20 months ago

Last modified 14 months ago

Connect Hets to SMV model checker (standalone version)

Reported by: till Owned by: hartke
Priority: critical Milestone: 0.95
Component: provers Version: 0.8
Keywords: Cc:

Description

To begin with, write a standalone tool:

  • Write printing syntax for LTL formulas that conforms to muSMV's syntax
  • code out W and R (which nuSMV does not know)
  • test for sublangange
  • Given muSMV model and LTL formula, call muSMV

Change History

Changed 20 months ago by till

  • summary changed from Connect Hets to SMV model checker to Connect Hets to SMV model checker (standalone version)

Changed 14 months ago by till

  • milestone changed from 0.9 to 0.93
Note: See TracTickets for help on using tickets.