ALTARICA: Details of all changes/forge/2014-01-29T10:48:02+01:00ALTARICAMcScM - Bug #72: Bad states are not checked/forge/issues/72?journal_id=1562014-01-29T10:48:02+01:00Tristan Le Galltlegall29@gmail.com
<ul><li><strong>% Done</strong> changed from <i>0</i> to <i>10</i></li></ul><p>Check bad states is implemented in current version of SCM. We need to update the version and test it when other eventual bugs are corrected.</p> McScM - Feature #58: Separate queue representation/forge/issues/58?journal_id=1082011-08-23T18:20:22+02:00Grégoire Sutregregoire.sutre@labri.fr
<ul><li><strong>Target version</strong> changed from <i>1.x</i> to <i>1.3</i></li></ul> McScM - Feature #26: Optimize scm cartesian product (or avoid it)/forge/issues/26?journal_id=1072011-08-23T18:20:00+02:00Grégoire Sutregregoire.sutre@labri.fr
<ul><li><strong>Target version</strong> changed from <i>1.x</i> to <i>1.3</i></li></ul> McScM - Feature #26: Optimize scm cartesian product (or avoid it)/forge/issues/26?journal_id=842011-06-23T12:33:01+02:00Tristan Le Galltlegall29@gmail.com
<ul><li><strong>Assignee</strong> changed from <i>Grégoire Sutre</i> to <i>Tristan Le Gall</i></li></ul> McScM - Bug #25: Scm consistency check takes too long/forge/issues/25?journal_id=832011-06-23T12:31:39+02:00Tristan Le Galltlegall29@gmail.com
<ul><li><strong>Assignee</strong> set to <i>Tristan Le Gall</i></li></ul> McScM - Bug #22: --help output not sensitive to terminal's characterwidth/forge/issues/22?journal_id=762011-04-08T13:45:43+02:00Grégoire Sutregregoire.sutre@labri.fr
<ul><li><strong>Target version</strong> set to <i>2.0</i></li><li><strong>Start date</strong> deleted (<strike><i>07/05/2010</i></strike>)</li></ul> McScM - Feature #21: redesign of command line parameters with respect to different checker-modules/forge/issues/21?journal_id=752011-04-08T13:45:00+02:00Grégoire Sutregregoire.sutre@labri.fr
<ul><li><strong>Target version</strong> set to <i>2.0</i></li><li><strong>Start date</strong> deleted (<strike><i>07/05/2010</i></strike>)</li></ul> McScM - Bug #25: Scm consistency check takes too long/forge/issues/25?journal_id=732011-04-08T13:42:53+02:00Grégoire Sutregregoire.sutre@labri.fr
<ul><li><strong>Target version</strong> set to <i>1.x</i></li><li><strong>Start date</strong> deleted (<strike><i>07/22/2010</i></strike>)</li></ul> McScM - Feature #26: Optimize scm cartesian product (or avoid it)/forge/issues/26?journal_id=722011-04-08T13:42:06+02:00Grégoire Sutregregoire.sutre@labri.fr
<ul><li><strong>Assignee</strong> set to <i>Grégoire Sutre</i></li><li><strong>Target version</strong> set to <i>1.x</i></li><li><strong>Start date</strong> deleted (<strike><i>07/22/2010</i></strike>)</li></ul> McScM - Feature #40: Source-code documentation (ocamldoc) in src/svar/forge/issues/40?journal_id=712011-04-08T13:40:43+02:00Grégoire Sutregregoire.sutre@labri.fr
<ul><li><strong>Target version</strong> set to <i>1.x</i></li></ul> McScM - Feature #29: Support Promela Input/forge/issues/29?journal_id=702011-04-08T13:39:47+02:00Grégoire Sutregregoire.sutre@labri.fr
<ul><li><strong>Status</strong> changed from <i>New</i> to <i>In Progress</i></li><li><strong>Priority</strong> changed from <i>Low</i> to <i>Normal</i></li><li><strong>Target version</strong> set to <i>2.0</i></li></ul> ALTARICA - Feature #7: Check monotonicity of Mec5 equations/forge/issues/7?journal_id=582011-03-17T10:29:23+01:00Gérald Pointpoint@labri.fr
<ul><li><strong>Target version</strong> changed from <i>1.4</i> to <i>1.5</i></li></ul> McScM - Feature #26: Optimize scm cartesian product (or avoid it)/forge/issues/26?journal_id=412010-07-22T15:54:52+02:00Grégoire Sutregregoire.sutre@labri.fr
<ul><li><strong>File</strong> <a href="/forge/attachments/45/petgen.4.scm">petgen.4.scm</a> added</li></ul><p>The attached file resembles the <em>peterson_3.scm</em> example, but with four processes. It was obtained by the following command :</p>
<pre>
python examples/other/peterson_generator.py 4 > petgen.4.scm
</pre>
<p>On this <em>petgen.4.scm</em> example, the computation of the cartesian product requires more that 2 GiB of RAM (on a 64-bit workstation) :</p>
<pre>
./bin/mcscm.native -verbose ./petgen.4.scm
MCSCM - Model Checker for Systems of Communicating Machines
Parsing input SCM description... done.
Computing global SCM by cartesian product of local systems...^C
</pre> McScM - Feature #21: redesign of command line parameters with respect to different checker-modules/forge/issues/21?journal_id=402010-07-06T15:35:25+02:00Grégoire Sutregregoire.sutre@labri.fr
<ul></ul><p>We should allow a configuration file that provides the same functionality as command-line options. As discussed, the format could be the one of Windows INI files (which is also used in e.g. kde, git, bazaar): <a class="external" href="http://en.wikipedia.org/wiki/INI_file">http://en.wikipedia.org/wiki/INI_file</a>.</p>
<pre>
[Module1]
option1 = foo1
option2 = false
option3 = true
[Module2]
option1 = toto2
option23 = truc
[Main]
verbose = true
</pre>
<p>The command-line equivalent would be:</p>
<pre>
-Module1 "option1=foo1:-option2:option3" -Module2 "option1=toto2:option23=truc" -Main "verbose"
</pre>
<p>The above example uses a shortcut syntax for booleans, but we could also write:</p>
<pre>
-Module1 "option1=foo1:option2=false:option3=true" -Module2 "option1=toto2:option23=truc" -Main "verbose=true"
</pre>
<p>For convenience, we should also allow simple command-line options that implicitly refer to the Main module. For instance, we could assume that options starting with an upper-case letter define module options, and options starting with a lower-case letter implicitly apply to Main.</p>
<p>We should allow command-line options even for (model-checking) modules that are not used (same for configuration file).</p>
<p>For documentation, I agree that -help should provide a minimal help (only options of the Main module?), and we could use -documentation to ask each module to dump a description of its configuration options.</p> ALTARICA - Feature #7: Check monotonicity of Mec5 equations/forge/issues/7?journal_id=112010-05-31T10:46:04+02:00Gérald Pointpoint@labri.fr
<ul><li><strong>Target version</strong> set to <i>1.4</i></li></ul>