Feature #26

Optimize scm cartesian product (or avoid it)

Added by Grégoire Sutre over 6 years ago. Updated over 5 years ago.

Status:New Start date:
Priority:Normal Due date:
Assignee:Tristan Le Gall % Done:

0%

Category:-
Target version:1.3

Description

McScM is only able to model-check flat 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.

Suggestions:
  • do not use string identifiers (of the form sender_0xreceiver_1x...), as they use a lot of memory.
  • perform the cartesian product in the Scm wrapper module.
  • compute the cartesian product on-the-fly (selectable by option)

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.

petgen.4.scm (13.3 kB) Grégoire Sutre, 07/22/2010 03:54 pm


Related issues

related to McScM - Feature #29: Support Promela Input In Progress 07/22/2010
related to McScM - Bug #25: Scm consistency check takes too long New

History

Updated by Grégoire Sutre over 6 years ago

The attached file resembles the peterson_3.scm example, but with four processes. It was obtained by the following command :

python examples/other/peterson_generator.py 4 > petgen.4.scm

On this petgen.4.scm example, the computation of the cartesian product requires more that 2 GiB of RAM (on a 64-bit workstation) :

./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

Updated by Grégoire Sutre almost 6 years ago

  • Assignee set to Grégoire Sutre
  • Target version set to 1.x
  • Start date deleted (07/22/2010)

Updated by Tristan Le Gall over 5 years ago

  • Assignee changed from Grégoire Sutre to Tristan Le Gall

Updated by Grégoire Sutre over 5 years ago

  • Target version changed from 1.x to 1.3

Also available in: Atom PDF