Translate executable with separate monoid

[mvdan]

Interestingly enough, the example below doesn't work if I run a compiled binary:

 $ ./dist/build/translate/translate examples/celement-concept-concat.hs
.model out
Segmentation fault (core dumped)

The same happens with the simulate executable. This must have something to do with hint.

This very reason keeps me from being able to reuse all the concept loading code between the two executables. If that code is not in the file given to runghc, it crashes. Haven't found a way around it yet.

 $ runghc translate/Main.hs examples/celement-concept-concat.hs
.model out
.outputs A B C
.graph
A0 A+
A+ A1
A1 A-
A- A0
B0 B+
B+ B1
B1 B-
B- B0
C0 C+
C+ C1
C1 C-
C- C0
A1 C+
C+ A1
A0 C-
C- A0
B1 C+
C+ B1
B0 C-
C- B0
C1 A-
A- C1
C0 A+
A+ C0
C1 B-
B- C1
C0 B+
B+ C0
.marking {A0 B0 C0}
.end

[mvdan]

@snowleopard feel free to propose a better file structure or module naming for all of this. I just went with the first thing that came to mind.

[snowleopard]

@mvdan Thanks, this is a good start.

I'd like to have a Haskell datatype corresponding to an STG, something like:

-- An STG transition comprising the signal a, the direction, and the occurrence number
data StgTransition a = StgTransition a Bool Int

-- Here a and b stand for the types of singnals and places
data Stg a b = Stg
    { stgName :: String -- corresponds to .model field in .g files
    , stgInputs :: [a]
    , stgOutputs :: [a]
    , stgInternal :: [a]
    , stgPlaces :: [b] -- there is no such field in .g files, but I think it's good to have it
    , stgProducingArcs :: [(StgTransition a, b)] -- arcs t -> p
    , stgConsumingArcs :: [(StgTransition a, b)] -- arcs t <- p
    , stgReadArcs :: [(StgTransition a, b)] -- arcs t <-> p
    , stgInitialMarking :: [b] }

And then it would be great to have a pure function toStg which does the conversion:

-- Our current translation uses places of type (a, Bool)
toStg :: CircuitConcept a -> String -> STG a (a, Bool)
toStg concept modelName = ...

Passing modelName feels a bit awkward, perhaps this should actually be stored inside concepts.

Actual printing of an STG should be done separately:

printDotG :: Stg String String -> String
printDotG = ...

The user need to translate an Stg a b to printable Stg String String manually, as relying on default Show instances can be problematic (e.g. default Show instance for (a, Bool) wouldn't work well).

I think this makes the API clean and reusable. Is this possible?

[snowleopard]

I just had a chat with @danilovesky and he suggested a lot of improvements to the above STG datatype. Briefly, it is better to model STGs as extensions of Petri Nets with specially labelled transitions. This could be done either by having data Stg a b = Stg { stgPetriNet :: PetriNet a b, ... } so it is possible to reuse the definition of PetriNet's, or via type classes class PetriNet a b => Stg a b where ... in which case it is also possible to apply functions operating on Petri Nets to STGs.

Hopefully, @danilovesky will provide a draft idea for how to structure the datatypes and/or classes :-)

[danilovesky]

I was thinking about something like this (excuse errors as Haskell is not my first language):

data Petri p t = Petri
    { name :: String
    , places :: [p]
    , transitions :: [t]
    , producingArcs :: [(t, p)]
    , consumingArcs :: [(p, t)]
    , readArcs :: [(p, t)]
    , initialMarking :: [p] }

data Stg p t a = Stg
    { petri :: Petri p t
    , inputs :: [a]
    , outputs :: [a]
    , internal :: [a],
    , label :: t -> (a, Bool) }

[snowleopard]

Thanks @danilovesky! I agree, this is better. Let me do another revision.

-- I dropped the name field, as it feels a bit awkward in this nice mathematical definition
data PetriNet p t = PetriNet
    { places        :: [(p, Int)] -- To support unsafe nets & avoid incorrect initialMarking 
    , transitions   :: [t]
    , producingArcs :: [(p, t)] -- I flipped p and t, I think it is likely to simplify coding
    , consumingArcs :: [(p, t)]
    , readArcs      :: [(p, t)] }

-- In general STGs may have dummy, s+, s- and s~ transitions
data StgLabel s = Dummy | Rise s | Fall s | Flip s

-- STG signal types
data SignalType = Input | Output | Internal

-- Here s stands for signals
data Stg p t s = Stg
    { petriNet  :: PetriNet p t
    , label     :: t -> StgLabel s
    , interface :: s -> SignalType }

We could also define the following intermediate datatype, which is a well-known mathematical object:

-- Here a stands for alphabet (of labels)
data LabelledPetriNet p t a = LabelledPetriNet
    { petriNet :: PetriNet p t
    , label    :: t -> a }

-- Then we could define STGs via LabelledPetriNet:
data Stg p t s = Stg
    { labelledPetriNet :: LabelledPetriNet p t (StgLabel s)
    , interface        :: s -> SignalType }

With Stg p t s datatype, @mvdan's algorithm should essentially correspond to:

-- Places are (s, Bool): signal and it's value
-- Transitions are (s, Bool): signals and directions: (s, True) ~ Rise s; (s, False) ~ Fall s
toStg :: CircuitConcept s -> Stg (s, Bool) (s, Bool) s
toStg concept = ...

[mvdan]

A couple of questions off the top of my head:

• What is the Int here for, exactly? If it's for the initial markings, I assume you want to use this instead of Bool for some particular reason?

    { places        :: [(p, Int)] -- To support unsafe nets & avoid incorrect initialMarking

• Why do we have transitions in the petri net and only classify them as Dummy/Rise/Fall/Flip at the STG level? Is this because petri nets have no such thing?

As for the work itself, I can either continue working on it and pushing commits here or do it in a separate MR if you'd prefer this merged first. Either way, the work will be on commits on top of the existing ones since otherwise it would be a lot of new code in a single commit.

[mvdan]

Also, the way that arcs are defined at the moment allows for duplicates. Is that OK in petri nets? If not, perhaps we would want to forbid it somehow, with something like a map or function? For example, we do forbid duplicate signal types with interface :: s -> SignalType instead of something like interface :: [(s, SignalType)].

[snowleopard]

What is the Int here for, exactly? If it's for the initial markings, I assume you want to use this instead of Bool for some particular reason?

Yes, and the reason is that PNs and STGs can have more than 1 token in a place. PNs/STGs with at most 1 token per place at any time are called safe.

Why do we have transitions in the petri net and only classify them as Dummy/Rise/Fall/Flip at the STG level? Is this because petri nets have no such thing?

So here is the hierarchy:

• PNs have no labels associated with transitions. They only have unique names and that's it.
• Labelled PNs have labels associated with transitions. These labels vary depending on particular applications, e.g. STGs have labels corresponding to signal changes.
• STGs have the notion of signals and signal types, and have labels corresponding to changes of these signals, as well as dummy labels, which have no observable effect on signals.

Note, the .g format supports all these features of STGs, so if we do export STGs to .g files we better support the general case, not the special kind of STGs that your algorithm produces.

Also, the way that arcs are defined at the moment allows for duplicates. Is that OK in petri nets?

I think it would be better to disallow duplicate arcs. However, your question revealed a missing bit in the above datatype: arcs can have weight in PNs. Normal arcs (the ones we typically use) have weight 1. An arc of weight 2 consumes/reads/produces two tokens from/to the place. So, we'll need to add some Ints.

Note also that the current definition allows duplicate places and transitions in the lists [(p, Int)] and [t]. So, we could in principle use Map p Int and Set t instead. It makes it a bit less convenient to operate with these datatypes (Haskell's syntax is optimised for lists), but it gives us more useful invariants. Let's go for Map and Set.

As for the work itself, I can either continue working on it and pushing commits here or do it in a separate MR if you'd prefer this merged first. Either way, the work will be on commits on top of the existing ones since otherwise it would be a lot of new code in a single commit.

Agreed, let's push this one and use these notes to build right reusable datatypes for PNs, LPNs & STGs.