fadysedrak / synoptic

Automatically exported from code.google.com/p/synoptic
0 stars 0 forks source link

InvariMint should output an error when the model is empty because of contradictory invariants. #226

Closed GoogleCodeExporter closed 9 years ago

GoogleCodeExporter commented 9 years ago
An intersection of contradictory invariant DFAs is the empty language. This 
should be considered an error and the code should catch it as soon as possible, 
and halt execution and alert the user when this happens.

Also, there should be a test case for this scenario (e.g., a AFby b intersected 
with a NFby b).

Original issue reported on code.google.com by bestchai on 24 Feb 2012 at 3:05

GoogleCodeExporter commented 9 years ago

Original comment by bestchai on 18 Apr 2012 at 7:28

GoogleCodeExporter commented 9 years ago
Addressed in revision 865bf592c8b6, please review

Original comment by jenny.abrahamson on 18 Apr 2012 at 7:30