Re: How to exchange high level net annotations

[Ekkart Kindler <kindler@informatik.hu-berlin.de>]

Dear all,

this is a response to some postings some weeks ago -- sorry
for the delay.

Kind regards,
Ekkart
--

1. There was some discussion on "flexible arcs".  Though I am
   in favour of having flexible arcs, I don't consider it as
   an attribute of the arc itself---in contrast to inhibitor or
   read arcs:
   It depends on the annotatation (arc-inscription) whether
   an arc is flexibel or not.  Thus, it depends on the constraints
   on annotations whether an arc is flexible or not (cf.
   contribution of Karsten Schmidt). 

   Therefore, I propose to delete all kinds of flexible arcs from
   the list of arc-types and make it an issue of high-level
   inscriptions, which is my next issue.  (However, there
   could be a different kind of label indicating that the arc is
   flexible---as proposed by Karsten Schmidt. This would help those
   tools that are not able to interprete the arc-inscriptions.)


2. I would like to put forward Karsten's proposals:
   I support Karsten's proposal to have as much common syntax
   (and semantics) for all high-level nets as possible.
   What we need is a format for
   a. defining new syntactical objects:
      * sorts  (this includes the definition of template sorts
                such as a stack over any given sort)
      * operation symbols
      Basically, we need a format for defining a signature.

      (I am not sure, where to place the definition of variables;
       they could be defined locally at each transition or globally
       for the whole net.)
       

   b. defining the semantics of these syntactical
      objects
      * a domain for a particular sort
      * a concrete operation (function) for an operation symbol

   In my opinion, a format for b. is out of range at the current
   stage. So, we should focus on a format for a.  Are there any
   proposals on this format? (If there are no proposals, I would
   choose some ACT ONE like format for signatures.)

   In order to have as much common syntax and semantics,
   we should fix some syntax and give it a fixed (common sense)
   semantics.
   Here is a proposal to start with (surely incomplete, but it
   gives an impression; names are subject to discussion):
   Predefined sorts:
      nat, int, bool, dot
      (where dot represents a sort with a single element: the
       black token)

      Maybe, there could be ranges; e.g.  int[1,..,27]

   Predefined template sorts:
      Pair, Triple, (Tuples in general), Bag
      (Bag(s) represents the bags---finite positive multisets---
       over sort s; maybe, we should call them multisets in order
       to meet the terminology of the PN standard;
       we could also include sequences, lists etc.)

   Predefined operations (and constants):
      d: -> dot

      true, false : -> bool
      not : bool -> bool
      and, or, implies, equiv: bool bool -> bool

      0, 1, 2, 3, ... : -> nat
      +, *, div, mod: nat nat -> nat          (how about - ?)
      =, <, <=, >, >= : nat nat -> bool

      ... -2, -1, 0, 1, 2, ... : -> int
      +, -, *, div, mod: int int -> int
      =, <, <=, >, >= : int int -> bool

 
      empty : -> Bag(s)
      + : Bag(s) Bag(s) -> Bag(s)             (how about - ?)
      =, <, <=, >, >= : Bag(s) Bag(s) -> bool
      Card : Bag(s) -> nat
      inj : s -> Bag(s)                (makes an element of
                                        s a singleton bag)
      * : nat Bag(s) -> Bag(s)         (scalar multiplication)
      count : Bag(s) s -> nat          (counts the number of
                                        occurrences of some
                                        element of s in a bag
                                        over s)

   Maybe, there could be some addiional conventions.  For example,
   a term t of sort s could be considered as inj(t) if a
   bag over s is expected ...

   Except for the operation . x . the corresponding Bag(s)-Terms
   give us non-flexible arcs.  As long as this
   operation is not used, Karsten's constraints on counting the 
   number of tokens (without knowing details on the datatype)
   is met.  I have included the scalar multiplication because
   it is in the PN standard.

   In this setting, a high-level net would consist of the
   following labels/annotations:
    - the net has a label representing the signature
      (maybe another label representing the variables)
    - each place has label representing its sort s and
      labels representing its initial and current marking
      (a Bag(s)-term).  A capacity could be represented also
      by a marking.
    - the corresponding arcs have a label (arc-inscriptions),
      which is Bag(s) term.
      This applies to all kinds of arcs (inhibitors, clear/reset,
      read and normal arcs).  I am not sure wether it is
      possible to have a default for arc-inscriptions in the
      case of high-level nets (maybe, it is inj(x) for some
      predefined variable x).
    - a transition can have a label that represents a guard,
      which is a term of sort bool (true is the default).