File Formats

This page contains file formats for I/0.

Format of Input Files

machine.fsm: Data for individual FSM.

machine.stoc: Stochastic data for machine.fsm.

glob_sens.map: Global sensor map for sensmap

sensor_datam.map: sensor data map for the system.

events.if: Events map for the system (I-diagnosability).

g.ft: Failure partition for building diagnoser

g.states: List of secret states for opacity

g.init: List of initial states for initial state opacity

Format of Output Files

g.fsm: Data for individual FSM (same as input FSM).

g.diag: Diagnoser of FSM.

h_diag.fsm: Diagnoser written in FSM format.

g.idiag: I-diagnoser of FSM.

g.sdiag: Diagnoser of FSM in simplified format.

h.cycles: Fi-indeterminate cycles in h.diag.

hi.cycles: (Fi,li)-indeterminate cycles in hi.diag.

g.states: List of states that violate opacity constraints.