mCRL2org / mCRL2

The Git repository for the mCRL2 toolset.
https://mcrl2.org/
Boost Software License 1.0
88 stars 37 forks source link

Dining philosophers examples broken #781

Closed jgroote closed 14 years ago

jgroote commented 14 years ago

Issue migrated from trac ticket # 777

component: mcrl22lps | priority: minor | resolution: fixed

2010-10-15 17:22:50: j.ketema@ewi.utwente.nl created the issue


When trying to linearize the dining philosophers examples in

examples/academic/dining

I get the following:

$mcrl22lps -v dining_10.mcrl2
reading input from file 'dining_10.mcrl2'...
type checking process specification...
applying alphabet reductions...
- process KForkPhil is a recursive parallel process in n-parallel pCRL format
error: the parameter in the process term KForkPhil(K) is not a concrete positive number.
error: Could not replace all npCRL processes (reason: init).
In this case alphabet reductions may not stop, or may not be performed completely.

I'm using revision 8266.

jgroote commented 14 years ago

2010-11-16 09:24:59: @jgroote changed status from new to closed

jgroote commented 14 years ago

2010-11-16 09:24:59: @jgroote set resolution to fixed

jgroote commented 14 years ago

2010-11-16 09:24:59: @jgroote commented


This problem was caused because dataspecifications transform themselves in appropriate format, a.o. by translating number strings into data expressions. The ad-hoc code for n parallel processes relied on numbers being strings. Data expressions are now translated back to strings, before the n parallel processes are expanded.

This should -for now- solve the problem.

jgroote commented 12 years ago

2012-08-24 07:05:07:

jgroote commented 12 years ago

2012-08-24 07:05:07: commented


Milestone To be decided deleted