Add a Dynoptic option to model check CFSMs with bounded queues

[GoogleCodeExporter]

By default McScM model checks CFSMs assuming infinite queues. However, this is 
often impractical -- we may only care about invariants being invalidated in 
some short trace, in say 100 or 1000 events.

Add an option to Dynoptic that bounds the queue size to a specific number of 
messages. Pass this option's value to McScM.

Original issue reported on code.google.com by bestchai on 6 Oct 2012 at 11:09

[GoogleCodeExporter]

Original comment by ssukkerd on 5 Nov 2012 at 11:05

• Changed state: Accepted

[GoogleCodeExporter]

McScM does not have an option to check CFSMs with bounded queues. See Issue 278.

Original comment by bestchai on 11 Nov 2012 at 8:26

• Changed state: Invalid