The current folder contains examples (models and scenarios) for scenario verification.

README: this file.
feas.cmd: script file that run the feasibibility analyisis
unfeas.cmd: script file that run the unfeasibibility analyisis
Subfolders:
  models: examples of hydi models that can be used for scenario
  verification.
  feasible: examples of feasible scenarios.
  unfeasible: examples of unfeasible scenarios.

Example to run both the analyses:
../../hycomp -pre cpp -source feas.cmd models/rod_2.hydi 
../../hycomp -pre cpp -source unfeas.cmd models/rod_2.hydi 

NOTE: the command files specifies also the path to the scenario file
to be verified. 

References to the scenario verification algorithms:
Alessandro Cimatti, Sergio Mover, Stefano Tonetta: SMT-based scenario verification for hybrid systems. Formal Methods in System Design 42(1): 46-66 (2013)
Alessandro Cimatti, Sergio Mover, Stefano Tonetta: Proving and explaining the unfeasibility of message sequence charts for hybrid systems. FMCAD 2011: 54-62
Alessandro Cimatti, Sergio Mover, Stefano Tonetta: Efficient Scenario Verification for Hybrid Automata. CAV 2011: 317-332

