[isabelle-dev] Duraraion of AFP session AODV

[Timothy Bourke]

Hi Florian,

* Florian Haftmann <florian.haftmann at informatik.tu-muenchen.de> [2014-11-27 11:59 +0100]:
> > This idea of variant models seems quite natural to me—one of the
> > advantages of mechanising such models and proofs is the ease of
> > experimenting with variations to the model—and I think it would be
> > worthwhile to solve the problem properly but I do not have any good
> > ideas for the present.
> 
> I guess you have already considered using locales to abstract over the
> different bootstrapping properties?

Locales have already been invaluable for tidying up other dependencies
(notably to separate AWN, the modelling formalism, from AODV, the
 model, and to avoid duplicating the final reasoning from an invariant
 over states to a property on routing graphs), but I couldn't see how
to apply them to the invariant proofs.

Basically, we have an automaton A with states of type S over which we
build up a succession of invariants. Then, we change A to A' and S to
S' and reestablish the invariants. Invariants are shown by cases over
every transition (scheme) in A. Some of them refer to specific control
locations within A/A'.

One possibility would be to encode all of the model variants within a
single automaton using parameters to switch on or off different parts
(like #ifdef's in C) and then to show the invariants for arbitrary
values of the parameters. This, however, would reduce the readability
and maintainability of an already complicated block of text.
 
> > 2. A handful of the sledgehammer generated proofs are quite intensive.
> >    I would like to fix these by doing more manual work (i.e., more
> >    steps in Isar), I just have to find the time.
> 
> So, a starting step would be to open the timing panel in Isabelle/jEdit
> and start working on the most time-consuming metis-proofs?  Would be a
> nice task for a maintainance volunteer.

That may be interesting, but, at least for AODV, these proofs can
already be identified since they stay 'purple' for so long! But maybe
it would be nice to display timing information in a popup bubble next
to the metis invocation?

Tim.

-------------- next part --------------
A non-text attachment was scrubbed...
Name: signature.asc
Type: application/pgp-signature
Size: 473 bytes
Desc: Digital signature
URL: <https://mailman46.in.tum.de/pipermail/isabelle-dev/attachments/20141127/c05aeed1/attachment.sig>