I need a formalism to describe the following requirements:
- I have a graph comprised of nodes and transitions between nodes
- Nodes maybe one of three types, all are sub-classes of a base abstract node type
- Activity nodes have one transition in and one out
- Wrapper nodes have one transition in and one out
- Routing nodes may have multiple transitions in and multiple transitions out
- Routing nodes can either behave as AND-join, AND-split, OR-split, OR-join depending on how they are configured
- Routing nodes can simultaneously be a join and a split, but not a join and a join, or a split and a split (obviously, since it can only join or split in one way)
- There are no cycles.
- There is only one root node - always a wrapper node - this is a source.
- Any node can be a sink/leaf where it has no outgoing transitions
- the terms Activity, Wrapper and Routing are just arbitrary names for classes in my graph that exhibit different behaviour and different semantics in terms of connecting them together
- the terms AND-join etc describe the way transitions connect to routing nodes - so AND-join means more than one transition is incoming. AND-split is where there are multiple outgoing transitions, OR-split is where there are multiple potential outgoing branches but only one is chosen, and OR-join is multiple potential transitions incoming, but only one is chosen.
I have almost no experience of formal models, though I'm guessing I need to use set notation and logical symbols.
What would a formalisation of the above requirements look like?
Thanks for any advice.