Got some kind of pretty print. Next up: edges, then pretty print
edges, then convert things to a decent format, then apply fernandez'
algorithm.
More pretty-printing, this time we are able to show all the
transitions as well.
Made module support for fernandez' algorithm, moved the old algorithm
implementation over. Planning to make an LTS out of the zone-valuation
graph next.
Moved some code around.
Added notes from the last meeting.
Added a function to generate a DOT file from a generic LTS.
Minor addition to .gitignore.
Working on making a module to represent a ZVG as a module.
Deleted a long comment.
Shifted some computation around, so that we now have zones in the zone
valuation graph (I know how it sounds) but only thise zones that are
actually reachable and only those which appear after transitions which
are actually doable.
Made ZVG compatible with LTS. Will merge now.
Made a graph, but a bad one.
Moved some code around, fixed some bugs.
Interface change in zone_stubs, just added a new function.
Interface change in zone_stubs, just added a new function.
Added a couple of functions and a relevant test.
Changing stuff to use new functions.
Changed an obvious error. We now have a more meaningful bisimilarity
relation on the ZVG, but it is still buggy.
Removed Fernandez_modules.ml from fernandez.nw. Makes things that much
easier to handle. The noweb comments can hopefully be scavenged, some
day.
Going to have to debug the LTS, committing for safety.