examples.segala.hs revision 98890889ffb2e8f6f722b00e265a211f13b5a861
c3d42e13d2a7c3749229498658aec34e7e4fd0a0Christian MaederModule : $EmptyHeader$
c3d42e13d2a7c3749229498658aec34e7e4fd0a0Christian MaederDescription : <optional short description entry>
cd7372fc7e6e43c389619f63daa6eb872d9d5b16Christian MaederCopyright : (c) <Authors or Affiliations>
98890889ffb2e8f6f722b00e265a211f13b5a861Corneliu-Claudiu ProdescuLicense : GPLv2 or higher, see LICENSE.txt
c3d42e13d2a7c3749229498658aec34e7e4fd0a0Christian MaederMaintainer : <email>
d5ef5a29a89fa5548f81fcd49fcf0ffda69d45b0Christian MaederStability : unstable | experimental | provisional | stable | frozen
d5ef5a29a89fa5548f81fcd49fcf0ffda69d45b0Christian MaederPortability : portable | non-portable (<reason>)
99c923311eab71a85f1dcc4785d349609c828da4Christian Maeder<optional description>
d5ef5a29a89fa5548f81fcd49fcf0ffda69d45b0Christian Maeder-- examples for Segala Systems. To run these examples,
120c9bff9059626735fc12b0399dcc9e5a62c345Christian Maeder-- one needs to run ``gen (flatten seg)'' from examples.gluings.hs
120c9bff9059626735fc12b0399dcc9e5a62c345Christian Maeder-- try both provable and sat(isfiable) from the (imported) module
d5ef5a29a89fa5548f81fcd49fcf0ffda69d45b0Christian Maeder-- MySat (generated as above) on the formulas defined here.
d5ef5a29a89fa5548f81fcd49fcf0ffda69d45b0Christian Maeder-- quickstart:
ce31795240d8fb340bc984b8b35147c955e29afaChristian Maeder-- gen (flatten seg) <-- generates MySat.hs; leave hugs
ce31795240d8fb340bc984b8b35147c955e29afaChristian Maeder-- and try provable and satisfiable on the formulas below.
3e603e36c535a7f0c7a6fe1c3f3b5768ab50853bChristian Maeder-- box 'a' phi is the HML-formula [a] phi
3e603e36c535a7f0c7a6fe1c3f3b5768ab50853bChristian Maederbox :: Char -> L1 -> L0; box c phi = HM0 c phi
1b0778e21d9b3e71a684ad6e901e8a0e7d57ee1cPaolo Torrini-- dia 'a' phi is the HML-formula <a> phi
3e603e36c535a7f0c7a6fe1c3f3b5768ab50853bChristian Maederdia :: Char -> L1 -> L0; dia c phi = neg (HM0 c (neg phi))
3e603e36c535a7f0c7a6fe1c3f3b5768ab50853bChristian Maeder-- l p phi is the PML-formula L_p phi
3e603e36c535a7f0c7a6fe1c3f3b5768ab50853bChristian Maederl :: Rational -> L0 -> L1; l r phi = P1 r phi
3e603e36c535a7f0c7a6fe1c3f3b5768ab50853bChristian Maeder-- example from the system description:
3e603e36c535a7f0c7a6fe1c3f3b5768ab50853bChristian Maederphi0 :: L0; phi0 = box 'i' ( (l (8%10) (dia 'i' (Atom1 0))) --> (l (5%10) (dia 'i' (Atom1 0))) )
3e603e36c535a7f0c7a6fe1c3f3b5768ab50853bChristian Maeder-- the two formulas used as example in Chapter 7.1 of
3e603e36c535a7f0c7a6fe1c3f3b5768ab50853bChristian Maeder-- ``Probabilistic Extensions of Process Algebras'' by Jonsson, Larsen and Yi
3e603e36c535a7f0c7a6fe1c3f3b5768ab50853bChristian Maeder-- (as argued in loc.cit., both are satisfiable but not provable)
3e603e36c535a7f0c7a6fe1c3f3b5768ab50853bChristian Maederphi1 :: L0; phi1 = dia 'i' ((l (7 % 10) (dia 'o' tt)) /\ (l (3 % 10) (dia 'e' tt)))
3e603e36c535a7f0c7a6fe1c3f3b5768ab50853bChristian Maederphi2 :: L0; phi2 = dia 'i' (l (9%10) (dia 'o' tt))