[ < ] | [ > ] |  | [ << ] | [ Up ] | [ >> ] |  |  |  |  | [Top] | [Contents] | [Index] | [ ? ]

# D. Examples

More examples can be found in the Maria source code, in the directory ‘`parser/test`’.

[ < ] | [ > ] |  | [ << ] | [ Up ] | [ >> ] |  |  |  |  | [Top] | [Contents] | [Index] | [ ? ]

## D.1 Dining Philosophers (‘`dining.pn`’)

    #!/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] | [ ? ]

## D.2 Distributed Database Management (‘`dbm.pn`’)

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 on January 22, 2026 using texi2html 1.82.