Hi Timothy, > 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
technical detail.
Cheers,
Florian
--
PGP available:
http://home.informatik.tu-muenchen.de/haftmann/pgp/florian_haftmann_at_informatik_tu_muenchen_de
signature.asc
Description: OpenPGP digital signature
_______________________________________________ isabelle-dev mailing list isabelle-...@in.tum.de https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev
