[ < ] | [ > ] | [ << ] | [ Up ] | [ >> ] | [Top] | [Contents] | [Index] | [ ? ] |
More examples can be found in the Maria source code, in the directory ‘parser/test’.
D.1 Dining Philosophers (‘dining.pn’) | Dining Philosophers | |
D.2 Distributed Database Management (‘dbm.pn’) | Distributed Database |
[ < ] | [ > ] | [ << ] | [ Up ] | [ >> ] | [Top] | [Contents] | [Index] | [ ? ] |
#!/usr/local/bin/maria typedef unsigned (1..5) philosopher; typedef struct { philosopher p, enum { thinking, hungry, eating } s } status; place fork (0..#philosopher) philosopher: philosopher p: p; place state (#philosopher) status: philosopher p: { p, thinking }; trans left in { place state: { p, thinking }; place fork: p; } out { place state: { p, hungry }; }; trans right in { place state: { p, hungry }; place fork: +p; } out { place state: { p, eating }; }; trans finish in { place state: { p, eating }; } out { place state: { p, thinking }; place fork: p, +p; }; |
[ < ] | [ > ] | [ << ] | [ Up ] | [ >> ] | [Top] | [Contents] | [Index] | [ ? ] |
The parameter of the model, the number of database agents, is only present in the data type definition. The initial marking expression and the arc expressions are independent of that parameter, thanks to the multi-set sum operator.
typedef unsigned (1..10) db_t; typedef struct { db_t first; db_t second; } db_pair_t; place waiting (0..1) db_t; place performing (0..#db_t-1) db_t; place inactive (0..#db_t) db_t: (db_t d: d) minus (place waiting union place performing); place exclusion (0..1) struct {}: (place waiting equals empty)#{}; place sent (0..#db_t-1) db_pair_t; place received (0..#db_t-1) db_pair_t; place acknowledged (0..#db_t-1) db_pair_t; place unused (1+#db_pair_t-2*#db_t,#db_pair_t-#db_t) db_pair_t: (db_pair_t p (p.first != p.second): p) minus (db_t t: (map s { place waiting } {s, t})); trans update_and_send_messages in { place inactive: s; place exclusion: {}; place unused: db_t t (t != s): { s, t }; } out { place waiting: s; place sent: db_t t (t != s): { s, t }; }; trans receive_acknowledgements in { place waiting: s; place acknowledged: db_t t (t != s): { s, t }; } out { place inactive: s; place exclusion: {}; place unused: db_t t (t != s): { s, t }; }; trans receive_message in { place inactive: r; place sent: { s, r }; } out { place performing: r; place received: { s, r }; } gate s != r; trans send_acknowledgement in { place performing: r; place received: { s, r }; } out { place inactive: r; place acknowledged: { s, r }; } gate s != r; |
[ << ] | [ >> ] | [Top] | [Contents] | [Index] | [ ? ] |
This document was generated by root on December 1, 2016 using texi2html 1.82.