McScM: Issues /forge/ 2014-03-19T09:02:41+01:00 ALTARICA Redmine Feature #82 (New): Learning-based algorithm /forge/issues/82 2014-03-19T09:02:41+01:00 Alexander Heußner <p>Add learning-based approaches for queue automata verification (see Vardhan et al. "Actively Learning to verify safety for fifo automata", FSTTCS'04 &#38; other publications of same authors).</p> Feature #81 (New): SCM++ (new automata definition language) /forge/issues/81 2014-03-19T09:00:05+01:00 Alexander Heußner Following some offline/email discussions, the following features would be a good start for a re-design/extension of the SCM input language: <ul> <li>more explicit keywords, e.g., for lossy</li> <li>abbreviations for some regular languages like \Sigma^*</li> <li>... (to be extended in discussion of this issue)</li> </ul> Feature #80 (New): JSON output of counter-examples /forge/issues/80 2014-03-19T08:58:01+01:00 Alexander Heußner <p>Due to user request: outputting the counter-examples in a simple, easily parsable format like JSON would be nice for external apps using McScM as plugin.</p> Feature #78 (New): SCM input language /forge/issues/78 2014-02-04T11:11:23+01:00 Tristan Le Gall tlegall29@gmail.com <p>une version du langage input avec<br />- quelques keywords plus explicites pour lossy etc.<br />- quelques abréviations pour des reguliers (\Sigma^*)<br />- des autres petites choses... (à collecter)<br />- fixer l'output de parser pour avoir des messages d'erreur syntaxe plus "lisibles"</p> Feature #73 (New): Better regular expressions /forge/issues/73 2012-08-08T15:31:03+02:00 Tristan Le Gall tlegall29@gmail.com <p>+ add a wildcard symbol<br />+ other improvements we could think about</p> Bug #72 (New): Bad states are not checked /forge/issues/72 2012-08-08T15:28:33+02:00 Tristan Le Gall tlegall29@gmail.com <p>1 in the SCM library, call the check_bad_states function</p> <p>2 modify the SVN revision of the SCM library in mcscm</p> Bug #59 (New): Account for k-max in trace-checking engines /forge/issues/59 2011-09-08T19:45:31+02:00 Grégoire Sutre gregoire.sutre@labri.fr <p>Trace-checking engines APInv/UPInv should abort if they must increase k beyond k_max to compute a trace invariant.</p> Feature #58 (New): Separate queue representation /forge/issues/58 2011-08-02T16:19:49+02:00 Tristan Le Gall tlegall29@gmail.com <p>Add an option for the representation of the queue contents, either<br />- QDD<br />- 1 automaton per queue</p> Feature #40 (New): Source-code documentation (ocamldoc) in src/svar /forge/issues/40 2011-04-04T11:20:47+02:00 Grégoire Sutre gregoire.sutre@labri.fr <p>Document all module signatures in the <code>src/svar</code> directory. In particular, transform the basic comments into ocamldoc ones in <code>src/svar/Model.mli</code>.</p> Feature #29 (In Progress): Support Promela Input /forge/issues/29 2010-07-22T20:23:18+02:00 Grégoire Sutre gregoire.sutre@labri.fr <p>Complete the Promela parser and connect it to McScM.</p> <p>This feature will require major changes to the tool :</p> <ul> <li>both input languages (SCM and Promela) should use the same semantics backend (Scm or directly LatticeAutomata).</li> <li>the Model signatures will have to be enriched to support some constructs of Promela (e.g. atomicity).</li> </ul> Feature #26 (New): Optimize scm cartesian product (or avoid it) /forge/issues/26 2010-07-22T15:42:07+02:00 Grégoire Sutre gregoire.sutre@labri.fr <p>McScM is only able to model-check <em>flat</em> models, i.e., models containing a single global automaton. To this end, the tool first computes the cartesian product of the local automata. This operation is crucial, and should be optimized.</p> <em>Suggestions</em>: <ul> <li>do not use string identifiers (of the form sender_0xreceiver_1x...), as they use a <strong>lot of memory</strong>.</li> <li>perform the cartesian product in the Scm wrapper module.</li> <li>compute the cartesian product on-the-fly (selectable by option)</li> </ul> <p>However, for realistic scm models with several machines, the cartesian product will simply be too large (for an explicit representation). In the future, McScM should avoid the cartesian product completely. To this end, the input to the model-checker functors will have to expose the local machines composing the model.</p> Bug #25 (New): Scm consistency check takes too long /forge/issues/25 2010-07-22T15:09:20+02:00 Grégoire Sutre gregoire.sutre@labri.fr <p>On large examples, the scm consistency check takes a very long time. The attached scripts produce scm models that are simple (no actions) but large.</p> <ul> <li>flat.scm.sh <em>size</em>: a single automaton with <em>size</em> locations and <em>size</em> transitions.</li> <li>product.scm.sh <em>size</em>: a product of <em>size</em> automata, each consisting of 2 locations and 2 transitions.</li> </ul> <p>The times in the table below have been obtained with the following commands (see attached files) :</p> <pre> sh flat.scm.sh &lt;size&gt; | mcscm.native -statistics sh product.scm.sh &lt;size&gt; | mcscm.native -statistics </pre> <p>On these examples (which do not have bad states), 95% of the total running time is taken by the scm consistency check. The table also contains an entry for the <em>peterson_3.scm</em> example, where 90% of the total running time is taken by the scm consistency check.</p> <table> <tr> <td></td> <th>Size</th> <th>Locations</th> <th>Transitions</th> <th>Consistency Check</th> </tr> <tr> <th style="text-align:center;" rowspan="3">Flat</th> <td>10000</td> <td>10000</td> <td>10000</td> <td>4.12 s</td> </tr> <tr> <td>20000</td> <td>20000</td> <td>20000</td> <td>21.45 s</td> </tr> <tr> <td>30000</td> <td>30000</td> <td>30000</td> <td>48.43 s</td> </tr> <tr> <th style="text-align:center;" rowspan="3">Product</th> <td>11</td> <td>2048</td> <td>22528</td> <td>2.24 s</td> </tr> <tr> <td>12</td> <td>4096</td> <td>49152</td> <td>15.14 s</td> </tr> <tr> <td>13</td> <td>8192</td> <td>106496</td> <td>80.88 s</td> </tr> <tr> <th>Peterson</th> <td>3</td> <td>10648</td> <td>56628</td> <td>37.80 s</td> </tr> </table> Bug #22 (New): --help output not sensitive to terminal's characterwidth /forge/issues/22 2010-07-05T19:22:36+02:00 Alexander Heußner <p>the output of the command line argument <code>--help</code> does ignore the width of the terminal and does line-wrap a lot on standard 80 character consoles; this makes the output pretty "unreadable".</p> Feature #21 (New): redesign of command line parameters with respect to different checker-modules /forge/issues/21 2010-07-05T19:19:54+02:00 Alexander Heußner <p>currently, all modules expect and accept the same parameters/arguments on the command-lines even if they ignore those that are not meant for themthemselves. i propose that we allow each "module" (i will call module the different verification algorithms implemented) its own parameters in addition to global parameters (like --help and -no-verification etc.).</p> <p>first ideas are to apply some kind of "mplayer" like syntax, that allow to give each module it's own, local parameters {{{<br />mcscm.native -cegar limit=10:split-simplificaiton=left:graph-exploration=bwd-bfs -no-verification -statistics<br />}}}</p> <p>this would also easily allow to use the same &lt;param&gt;=&lt;value&gt; syntax for a simple cfg file ;-)</p> some open questions: <ul> <li>does one need to additionally choose the mc-engine ? (hence, can there be params for engines that i do not use?)</li> <li>what other syntaxes could be possible ?</li> <li>what is possible with standard OCaml features ?</li> <li>how to present this "nicely" when using --help (idea: clean up --help to a minimum and use a --long-help or --documentation for a long, man-like help feedback)</li> </ul>