Open jgroote opened 12 years ago
The examples with n parallel dining philosophers are removed from the toolset. The example with 10000 processes is attached to this ticket such that it is not forgotten, and can be reallowed in due time.
dining_10000.mcrl2
(0.9 KiB)
Issue migrated from trac ticket # 977
component: Core: Alpha Library | priority: minor
2012-02-04 11:26:08: anonymous created the issue
By translating the alphabet reduction framework from ATerms to the new data types, the code to deal with n parallel processes has been removed. However, there are a number of examples, such as 100, 1000 or even 10000 parallel dining philosophers that essentially depended on this construct.
This feature should be restored, probably by adding special syntax to allow this.