[isabelle-dev] Duraraion of AFP session AODV
florian.haftmann at informatik.tu-muenchen.de
Thu Dec 4 09:40:10 CET 2014
> 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.
no, it does not sound good indeed to clutter a specification with such
-------------- next part --------------
A non-text attachment was scrubbed...
Size: 181 bytes
Desc: OpenPGP digital signature
More information about the isabelle-dev