At last... LaTeX inside Dot inside LaTeX

[compilerbitch]

I managed to get dot to draw a diagram where the boxes contained LaTeX formulae today:



A Haas diagram showing the lattice of values of my 15-value logic with respect to subset membership

The trick was to fire up LaTeX once for each bubble, with only the content of the bubble on the page (i.e. no headings/page numbers/etc.), then to use dvips -E to generate EPS with a tight bounding box. Getting dot to use these images was easy -- for each node, set the shape to epsf and specify the relevant EPS file. I then made dot export the whole diagram as an EPS, which allowed me to integrate it into a big LaTeX document. (As a slight aside, the whole document, diagrams and all is built by a single 500 line ML program).

I am such a geek. Someone slap me.

Comments

Re:

[compilerbitch.livejournal.com]

Oh, this is pretty obscure stuff. I'm working on a number of possible alternative multivalue logics that can prove interesting things about the properties of digital circuits. The idea is twofold, with the main bit being extending Boolean logic with extra values that capture state changes (the existing false and true represent 'steady state forever') values. The second trick is to define time in a peculiar way -- time is linear, continuous and dense, with the structure (but not the arithmetic) of the real numbers. When you do that, you can define a whole menagerie of weird new logics that can do useful stunts, like tell you that a and not a is not actually equal to False (rather, False is a subset of the possible behaviour, with various nasty glitches also being possible).

There is a 'master' logic that has an effectively infinite number of possible values, which forms the underlying model for all of my representations. The next simplest is an evil little thing with 256 values that is very powerful and very general, but a bit of a handful without machine assistance. So I set to work finding a number of simpler logics with rather more tractable characteristics. So far I have logics with 1, 2, 3, 5, 7, 9, 11, 13 and 15 values, some of which are more useful than others, but all of them form a hierarchy with Galois connections back to the master logic. That is, the bigger more complex logics can answer some questions that the simpler ones give up on, but when any of the simple logics give an answer, the more complex logics are constrained by that. To prove all of this, I need to take a lattice theoretic approach, so the Haas diagrams for each logic have to be calculated and shown to correspond to each other (hence the Galois theory). Figuring out Haas diagrams is a sod at the best of times, and when I have about 20 of them to draw (accurately!), hacking visualisation tools like dot (part of the AT&T Graphviz system) turns out to be well worth it. I have an ML program which when given a list of logics automatically spits out truth tables and Haas diagrams for each one. Eventually, it will hopefully also spit out a decent collection of algebraic laws, and hopefully also proof systems for each logic.

Turn the handle, out pops a thesis chapter, basically!

[fluffymark]

Is that such a peculiar way to define time? I would think it natural to define time as linear, continuous and dense. And having the structure but not arithmetic of real numbers seems likely too.

Does a 1-value logic make any sense at all, other than the totally trivial: (True == True) == True ?

Why is 256 values special? (other than being 2^8)

Re:

[compilerbitch.livejournal.com]

Is that such a peculiar way to define time? I would think it natural to define time as linear, continuous and dense. And having the structure but not arithmetic of real numbers seems likely too.

To a physicist it probably seems obvious to do that, but compscis tend to be wedded to discrete time. Nearly all of the theory in this area is based on parallel finite state machines, with an assumption that there exists a discrete clock rate fast enough that only one transition happens during one clock interval. It's relatively rare to take a dense time approach, but there are big advantages (e.g. you get to look at all possible relative timings at once without having to enumerate them).

Does a 1-value logic make any sense at all, other than the totally trivial: (True == True) == True ?

Actually, I'd disallow that logic because it has an element whose negation is not definable (e.g. there is no possible result for 'not true'). Most of my logics (all the useful ones anyway!) have a top element that represents 'the set of all possible signals', drawn as a star (you can see it in the Haas diagram I posted). My one value logic is totally useless in and of itself, in that it defines 'not star = star, star and star = star, star or star = star'. It does come in handy in defining the hierarchy of Galois connections though because it is a bottom element for the lattice of logics.

Why is 256 values special? (other than being 2^8)

Aha, I thought that might poke you! The four basic values are false, true, up and down (where up is false becoming true, down is true becoming false). Each of these come in two flavours: clean and dirty, indicating whether or not the transition or steady state has any glitches superimposed on it. This gives 8 values, but it's not quite enough on its own. The problem comes in defining, for example, 'up and down', which depending on relative timing might represent either clean false or dirty false. It is therefore essential that the representation must be able to handle nondeterminism. Following Cousot & Cousots abstract interpretation ideas, this is just defined by taking the power set of those eight values, giving the set of all possible nondeterministic choices. 256 of them, to be specific. I'm pretty sure this is a closed abelian group with respect to 'and' and 'or', with negation doing the obvious thing, but my group theory is a bit vague I'm afraid. The other logics basically have different subsets of these 256 values mapped to the top element -- it's actually quite surprising how far you can go with that and still keep nearly all of the functionality of the 256 value logic.

The infinitary logic is more powerful still, in that it can not only tell you if something can glitch, but it can also tell you how many times it can glitch. This is probably going to spawn a probabilistic variant that can be used for power estimation (power in CMOS circuits is typically proportional to the number of switchings per unit time, so glitches cost power in a big way).

[fluffymark]

Oh wow. yes. Your diagram makes sense now. Apart from the meanings of S and C, I think I can follow it.

Re:

[compilerbitch.livejournal.com]

S = static, i.e. the value might be steady state true or steady state false, but it never transitions.

C = clean, i.e. the value might be clean false, true, up or down, but may never be dirty.

These values are a bit experimental, quite a recent idea actually. They can handle two important classes of signal that happen in real circuits, specifically signals that are unknown at design time but unchanging at run time (e.g. the contents of flash memory configuration, etc.), and signals that must be clean, such as clocks in synchronous circuits or pretty much anything in asynchronous circuits.

Re:

[fluffymark]

I must have been thinking about that diagram in my sleep, as I woke up realising that S meant static and C meant clean.

Re:

[compilerbitch.livejournal.com]

You can kind-of figure it out from the diagram, but well done for spotting it!

I'm planning to add a bunch of other operators that can't be defined directly in conventional logics, e.g. D-type flip flops, SR latches, C elements, etc. so I can have a go at deriving algebraic laws for manipulating circuits that contain them. I'm also planning on having a go at embedding these logics in a more sophisticated dense continuous time interval temporal logic for model checking purposes. It's fun so far...!