/usr/share/doc/maria/examples/dbm.pn is in maria 1.3.5-4.
This file is owned by root:root, with mode 0o644.
The actual contents of the file can be viewed below.
1 2 3 4 5 6 7 8 9 10 11 12 13 14 15 16 17 18 19 20 21 22 23 24 25 26 27 28 29 30 31 32 33 34 35 36 37 38 39 40 41 42 43 44 45 46 47 48 49 50 51 52 53 54 55 56 57 58 59 60 61 62 63 64 65 66 67 68 69 70 71 72 73 74 75 76 77 | // Distributed data base management model for Maria by Marko Mäkelä
// First presented by Genrich and Lautenbach; later by Jensen
// Use -DUNUSED to enable the redundant place named "unused"
// Use -DPRIORITY to enable prioritized treatment of "receive message"
typedef id[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;
#ifdef UNUSED
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}));
#endif // UNUSED
trans "update and send messages"
in {
place inactive: s;
place exclusion: {};
#ifdef UNUSED
place unused: db_t t (t != s): { s, t };
#endif // UNUSED
}
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: {};
#ifdef UNUSED
place unused: db_t t (t != s): { s, t };
#endif // UNUSED
};
trans "receive message"
#ifdef PRIORITY
!
#endif // PRIORITY
in {
place inactive: r;
place sent: { s, r };
}
out {
place performing: r;
place received: { s, r };
};
trans "send acknowledgement"
in {
place performing: r;
place received: { s, r };
}
out {
place inactive: r;
place acknowledged: { s, r };
};
|