PVS Example: Tabular Specifications and SCR Model Checking Description: csl-95-12.dvi.Z csl-95-12.ps.gz NOTE (4/26/96): Following haven't been checked with released version of the system owing to file system problems Presents four sets of examples: 1. Simple tables and their well-formedness TCCs (Report Chapter 1) Dump file: simple_tables.dmp Use PVS command M-x undump-file simple_tables.dmp 2. Decision Tables (Report Section 3.2) Dump file: decision_tables.dmp Use PVS command M-x undump-file decision_tables.dmp 3. SCR mode transition table and model checking (Report Sections 4.1 and 4.2 -- uses Atlee and Gannon's automobile cruise control example) Dump file: cruise.dmp Use PVS command M-x undump-file cruise.dmp 4. Interacting transition relations and trace-equivalence checking (Report Section 4.3) Dump file: autopilot.dmp Use PVS command M-x undump-file autopilot.dmp