Exercise: Logic Circuit Advanced

In this exercise, we will be improving on our previous implementation of a logic circuit. Think back to how we represented the circuit. Was anything wrong with it? Are there things that you feel could be improved?

▶ Answer

The idea behind this advanced implementation is to be more generic by not hard-coding our wires, but by instead describing the behavior of each type of gate and their connected wires. For this, we will be using the following vocabulary:

vocabulary V { type gate := {A, B, C, D, E} type wire := {K, L, N, M, O, P, Q, R} AND: (gate) -> Bool OR: (gate) -> Bool XOR: (gate) -> Bool FirstInput: (gate) -> wire SecondInput: (gate) -> wire Output: (gate) -> wire On: (wire) -> Bool StartOn: (wire) -> Bool StartOff: (wire) -> Bool }

In this vocabulary, we will represent both gates and wires using a type.

To know the type of each gate, we introduce the predicates AND, OR and XOR.
As each gate is connected to three wires (2 inputs and 1 output), we need a way of "connecting" them. FirstInput, SecondInput and Output are functions mapping each gate to these wires.
To know the status of each wire, we use the On predicate. Because we also need a way to know which wires are toggled on/off in the interactive diagram, we also add StartOn and StartOff.

Most of the symbols introduced in the vocabulary are already fully interpreted, i.e., we already know their values. As such, we can add these interpretations to our structure. Based on the diagram below, try to complete the following structure. To help you out, we already filled in the values of FirstInput:

structure S:V { FirstInput := {A -> K, B -> N, C -> L, D -> M, E -> Q}. SecondInput := { }. Output := { }. AND := { }. XOR := { }. OR := { }. }

▶ Answer

structure S:V {
  FirstInput := {A -> K, B -> N, C -> L, D -> M, E -> Q}.
  SecondInput := {A -> L, B -> M, C -> K, D -> N, E -> O}.
  Output := {A -> N, B -> P, C -> O, D -> Q, E -> R}.
  AND := {C, D}.
  XOR := {A, B}.
  OR := {E}.
}

Now all that remains is our theory. We need to express two things:

Any wire that is on at the start is on, and any wire that is off at the start is not on.
For each gate we need to express their behavior in terms of their connected wires.

Like in the last exercise, try out your formula by clicking on the names of the wires in the diagram above.

theory T:V { }