search

kind2-mc / kind2

Multi-engine SMT-based automatic model checker for safety properties of Lustre programs
https://kind.cs.uiowa.edu
Apache License 2.0
88 stars 29 forks source link

Add --lus_main_type flag and give info about type declarations in LSP info #1075

Closed lorchrob closed 5 months ago

lorchrob commented 5 months ago
  1. Add flag --lus_main_type which allows the user to specify a main type for realizability checking
  2. Augment the LSP info to include whether or not the main type contains some refinement type