[Date Prev][Date Next][Thread Prev][Thread Next][Date Index][Thread Index]
[tlaplus] composing specifications
- From: ns <nedsri1988@xxxxxxxxx>
- Date: Wed, 16 Mar 2022 21:09:44 -0700 (PDT)
- Ironport-data: A9a23:IFUoKaujEqJKe/dbdX1KAxIDmefnVPhbMUV32f8akzHdYApBsoF/q tZmKWGPaPaOYjane9wnPNni8U8D7ZDTytNnQQI9+Hs8En4QgMeUXt7xwmXYb3rDdJWbJK5Ex 5xDMYeYdJhcolv0/ErF3m3J9CEkvU2wbuOgTraCY0idfCc8IMsboUsLd9UR38g52bBVPyvX4 Ymo+5aGZwf8s9JJGjt8B5yr+EsHUMva42twUmwWPZina3eD/5W9JMt3yZCZdxMUcKEMdgKJb 7qrIIWCw4/s10xF5uVJPVrMWhZirrb6ZWBig5fNMkSoqkAqSicais7XOBeAAKtao23hojx/9 DlCna6CSB8zL7XXotkMSgZlGi1AEI1vpLCSdBBTseTLp6HHW37lwvErC0ZveINGpqB4BmZB8 fFeIzcIBvyBr7jukfTrF6812J1lcpWD0IA34hmMyRnFCf8+RY3YAK/M7vVz/wUCpJ1qJ9/zT eAyURhdTzX5RjJ2F24uVa4Os9aAiX74fDlVp0iSuLIspWPUyWSd1ZC3boeIJYXTHq25mG69n 030wDrEMipDOd6T8TuH0V2mis7AyHaTtIU6TeXkrJaGmma7ym0IAwANTnOnpfD/j1WkHtNZM U0dvCsot6k7skKxJuQRRDW9qX+A+xkbAp9eTbF85waKxa7ZpQ2eAwDoUwKtdvQUhs4uXy0yz WW0jsr2ODVjjpC1YC6So+L8QSyJBQAZKmoLZCkhRAQD4sX+rIxbsv4pZoYzeEJSpo2lcQwc0 wxmvwBl3ehK1pdjO7GTuAGa0mrz/PAlWyZsvl2PNl9J+D+Vc2JMi2aAwlHd8fFGRGpyZgbc5 SBf8yRyARxnMH1gvCmEQeFIG7bwovjbbHvThllgG5Rn/DOok5JCQWyyyG4lTKuKGpxeEdMMX KM1kV4JjHO0FCbyBZKbm6rrV6wXIVHITLwJrMz8YNtUeYRWfwSa5ixobkP49zmzzBdwzPxjY c7BL57E4ZMm5UJPnGreqwA1ge9D+8zC7T67qW3Tk0z3gOPGOhZ5t59caQfSMojVE59oUC2Mq 4oFXyd74xpYV+L6b0HqHX07fDg3wYwALcGmw+QOLrDrClM/RAkJVqGNqZt8Jd0Nt/kFx4/go yDhMmcFmQqXrSOcc22iNCszAI4DqL4jxZ7NFXF3YwbANrlKSd3H0ZrzgLNsJOh5rrM/laAoJ xTHEu3Zaslypv3802x1RfHAQEZKLnxHXCqCYHioZiYRZZllS1Cb89PoZFKxpiYJCSWzuMQkp KC4zUXQRp9aH1ZuC8PfafSOyVKtvClNw7krBBSWfdQDKl/x9IVKKjDqiqNlKc87LxielCCR0 BybAEtFqOSU+901/dDFiLqqtYCsF+ciTENWE3OKv7mzPCjeuGGkxNYYAuqPeDncUkLy+bmjN b0FlaGibKVfkQ8T4YRmErttwaYv3PfVpudXnlZ+AXHGT1W3Ebc/cHSL2M94sKcSlLJUvA2BX F3WpotXNLCPD8PSEFALIT0jYOneh+ofnSPf7KhsLUj3vXQl/LeOXUhIBRSUjD1BK795bNEsz es74ZBE5Au4hR4nPcyBkzhPsW+LKyVYAakgs5gbBq7tixYqmwEZOsWHVXGp7cHdcchIP2krP iSQ2PjIiYNayxeQaHE0D3XMgbdQiJlS6hBHyFgOewaAltbf3KRl2RRQ9XEwSV0QwEsble10P WdvOgt+IqDXp2Vkg81KXmaNHQBdBU3GphaglQNRzGCJHVO1UmHtLXEmPbrf9k4u9W8BLCNQ+ 6uVyTq4XDu7LsXwxTcPX1V4ofjvEY54+gHYxpD1Gs2EG4U9MzXihaCqaGUSrAb/GoY0jUvOq uQpp7kgOPGma35P+vRlSJSczqkaUxueJWZPaf5m+6wNEG7Gfyyqwn6FLEXoIpFBIPnD8EmZD c1yJ5MfDE/nj3nQ8T1LV7QRJ7JUneIy4IZQcL3cI2Nb4aCUqSBksc6N+yXy2D0iT9l0zZdvK p/NbynQVSufn3xJg3SLo85DNW61J9IDYUrzxueo6KIVE5sbtPx3Nlov2KC/pXSfPQZqo0COs AXYa/OExuBu0943zY7lE6EGAALtbN2tCKKH9we8t9kIZtTKaJ+cuwQQo1jhHgJXIbpBBIgtx OrV6Ib6jBHfobI7c2HFgJ3dRaNH0sO/AbhMOcXtIXgGwCaPVacAOffYF7xU9HCIrD9c2iVjb w6xac/1ctlMHtkDmDtabC9RFxtbAKPyBkslSeVRsNzUYiXxEySeRD9kyZMtRW5ccSAMNpLkD RLsoLCl4dUwQEFkGkofH/8/a3NnCAaLZEblHuEdcRGXCW6nhl6NoLz/jQFm4jbOYpVB/AAW/ rqdLiXDmN+OVG0kAT2XX0GefvHaMZqlvdQNQw==
- Ironport-hdrordr: A9a23:UBKOMawxb1wcKL9mYuIBKrPws71zdoMgy1knxilNoH1uA7alfq WV9pkmPHDP+VIssR0b6Le90EfpewKpyXZaibNhSItKHzOWyVdBFelZnPnfKkTbalrDH41mpN xdmx0UMqyPMbEFt7eC3ODiKade/DDvysnB7pa9854Kd3AXV0hO1WhE422gYzVLrWd9dPwE/F v13Lslm9NiQxoqhwaAakXs74P41q72fV7dACLv93UcmXSzZPqTiM+eLzGomi0GWzcK67Yv+2 rInkjY4eGMqPem03bnph/u06g=
- Ironport-sdr: HeO6Zln04JxNnTbVK7LkpNu1PLvCOZ4R5VRKaoImosjWJtrSaq46voJCBMq9w3EjVP9Iur/Yyk ii4tTFElOQi3EYXGg3YtI+JqOJ3XTyVLNBuiDJBaU0O0OQS5P559wyS0r26D1qjiV7W/oeL4Xj QhiLsGFJCSwVg8SmKWzdVgfxR/u7z7LtLlMuCyzKOaPC1xaO+mLICMEYGzzvpncv656V0Me/2L 7nIiSYDU+watND05agoBHLFCki5bwb0GtbHyzU0BsaZVsbK7pK6u9OX5Ddj57jI9PreC528gcK VOW3Nna9FXvDfm5526rUagv7
I have a question from reading Sec. 10.4.1 of the S.S. book There it talks about composition in the presence of shared updatable state. The example is of a Sender and Receiver system communicating using a shared buf. I understand that if you have a monolithic spec then it would be written InitSR /\ [][NextSR]_<<s,r,buf>> (ignoring fairness for now), where SR == Sndr \/ Rcvr, defined in the book, specifically Sndr mentions r and Rcvr mentions s where s and r are the sender and receiver state vars resp. He then (I assume) wants to defines the system as the composition of two components Cs /\ Cr, where Cs = Init_S /\ [][NS]_<<s,buf>> and Cr == Init_R /\ [][NR]_<<r,buf>>. So
Cs /\ Cr == Init_S /\ Init_R /\ [][NS]_<<s,buf>> /\ [][NR]_<<r,buf>>. The form of say NS is given as Sndr \/ (sigma /\ (s'=s)), where sigma is calculated. The problem is that this still requires the component Cs know about r (and correspondingly Cr knows about s) How is this possible if Cs and Cr are two separate components? Does r represent the "environment" in an assume-guarantee setting?
--
You received this message because you are subscribed to the Google Groups "tlaplus" group.
To unsubscribe from this group and stop receiving emails from it, send an email to tlaplus+unsubscribe@xxxxxxxxxxxxxxxx.
To view this discussion on the web visit https://groups.google.com/d/msgid/tlaplus/689ec68a-2a5b-44d4-a380-0b033f28a42an%40googlegroups.com.