WIP: Added dual for toggling transitions.

[jrbeaumont]

This is branched from the PR #75, so I will highlight the new function.

flipSpec is a function which takes a concept specification and returns a concept specification where all transitions are opposite. This is mainly for some interest.

Testing proves our expectations: flipSpec $ orGate a b c produces and AND-gate flipSpec $ andGate a b c produces an OR-gate flipSpec $ cElement a b c produces a C-element and this is the same for a C-element with environment example.

Any further suggestions for testing?

[snowleopard]

Let's call this function dual, I think it's common to think of AND and OR gates as duals.

[jrbeaumont]

Renamed.

[jrbeaumont]

I have changed the implementation, this is much nicer :)

Do we need to add a dual function for another field? Transitions can be flipped, so possibly can initial states. Interface cannot really, but invariants might?

[snowleopard]

Yes, I think we should also flip the initial states and the invariant. The interface seems to be unaffected.

[snowleopard]

With these changes the dual of the ME element will probably be the RS latch, i.e. two NOR gates instead of two NAND gates, with correct invariants and initial states.

[jrbeaumont]

I will implement these changes and test it.

[jrbeaumont]

@snowleopard I am having issues with implementing dualInitialState. Because we defined in Concept that initial = a -> InitialValue, and this function is defined before we introduce Signal, I cannot work out how to access each InitialValue, as we need an a to get the -> InitialValue, so I can then get the defined initial state (if it is defined correctly) and then negate it.

[snowleopard]

Will something like this work?

dualInitial :: (a -> InitialValue) -> (a -> InitialValue)
dualInitial f = dualValue . f

dualValue :: InitialValue -> InitialValue
dualValue (Defined v) = Defined (not v)
dualValue x = x

[jrbeaumont]

Perfectly. I had the right idea, just the wrong implementation. Was just struggling to find a way of accessing it without using a signal.

[jrbeaumont]

@snowleopard I have implemented those. Also I accidentally added the flip branch to the main repo. My bad, computer switch and muscle memory.

[jrbeaumont]

Testing: Using the file:

module Concept where

import Tuura.Concept.STG

circuit a b c = interface <> andGate a b c <> initialState <> never [rise a, rise b]
  where
    interface = inputs [a, b] <> outputs [c]

    initialState = initialise a False <> initialise b False <> initialise c False

This without dual creates an AND-gate STG, which should never allow a+ and b+ within initial states 0. The output of plato is:

.model out
.inputs A B
.outputs C
.internal 
.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
C1 C-/1
C-/1 C0
A0 C-
C- A0
B0 C-/1
C-/1 B0
A1 C+
C+ A1
B1 C+
C+ B1
.marking {A0 B0 C0}
.end
invariant = not (A && B)

If we add in dual $ before the rest of the concept description, and translate this:

.model out
.inputs A B
.outputs C
.internal 
.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
A0 C-
C- A0
B0 C-
C- B0
C0 C+/1
C+/1 C1
A1 C+
C+ A1
B1 C+/1
C+/1 B1
.marking {A1 B1 C1}
.end
invariant = not (not A && not B)

Notice, the invariant is now not (not A && not B) indicating the dual of the invariant. Also, notice that the initial markings are now A1 B1 C1 instead of all 0.

[snowleopard]

Cool!

Just an idea: I think we can make the definition very symmetric:

...
           initial = fmap dualValue (initial c),
           arcs = fmap dualCausality (arcs c),
           interface = interface c,
           invariant = fmap dualInvariant (invariant c)
...

Could you check if it works? If yes, think why it works :-)

Also, if it does work, drop dualInitial, rename dualValue to dualInitialValue, and we'll have a very symmetric solution.

[jrbeaumont]

This does work! So I believe it works because it applies the change to each function of the field here. So because it is a -> InitialValue treats every outcome of the function, because it is finite and can be determined. This applies to arcs and invariant too because there is no function to find the Causality [e] e and Invariant e, so all outcomes can be definitely determined.

[snowleopard]

@jrbeaumont Cool :-)

So, I suggest you look up the definition of Functor type class in Haskell, and see how it is implemented for lists (where fmap = map) and for functions (where fmap = (.)). Then this should be even clearer.

You can start here: http://learnyouahaskell.com/making-our-own-types-and-typeclasses#the-functor-typeclass

[jrbeaumont]

I will read that now. If you would like this merging we need to wait until #75 is merged unfortunately.

[snowleopard]

OK, just ping me when this can be merged.

[jrbeaumont]

OK thanks.

I believe the other may be mergeable now. More changes can be made but we can do it in a future PR.

[jrbeaumont]

Comments have been added in this branch, to include the new dual in the commenting. Any suggestions are welcome, of course. When merging, we will need to merge #75 first, then this pull request.

[snowleopard]

Thanks, good job! Just one minor comment about consistency loops.

[jrbeaumont]

I will sort the loops references and then this is ready to merge. I will merge this one.

[snowleopard]

There are now some merge conflicts, so I guess you'll need to rebase. Happy to have a final look.

[jrbeaumont]

Yes I imagined this might happen. I will ping you when I have resolved.

[jrbeaumont]

@snowleopard: Merge issues fixed, comments updated.

[snowleopard]

Great, thanks! Now merged.