[Date Prev][Date Next][Thread Prev][Thread Next][Date Index][Thread Index]
Re: [tlaplus] TLA+ video course: Can't add invariants/property from imported module
- From: Markus Kuppe <tlaplus-google-group@xxxxxxxxxxx>
- Date: Wed, 25 May 2022 21:00:42 -0700
- Ironport-data: A9a23:+duBnahuc6lsCTK/V7wE+yXnX161mxUKZh0ujC45NGQN5FlHY01je htvXGuCa62NZzf8co90Odmw908EsZaDy99iTlZkqCBhRS1jpJueD7x1DG+gZnLIdpWroGFPt phFNIGYdKjYaleG+39B55C49SEUOZmgH+a6UKieUsxIbVcMpB0J0HqPoMZkxN8x6TSFK1nV4 4mq/peCYAXNNwNcawr41YrT8HuDg9yp4Fv0jnRmDRyclAK2e9E9VfrzFInpR5fKatE88t2SG 44v+IqEElbxpH/BPD8KfoHTKSXmSpaKVeSHZ+E/t6KK2nCurQRquko32WZ1hUp/0120c95NJ Npl6oC0Y1YJYoD3hcsQQzdhKyRVPLJl9+qSSZS/mZT7I0zudnLtx7BxCRhzM9BFvOlwBm5K+ LoTLzVlghKr3brnhuLmDLA21oJ+caEHP6tH0p1k5S3dBO4iXIuASaPBz/R47g8ftux+NN/kT ZY5VgpITz3lTCRiHmw1MrQctc+ngX7wdzBXslWIvbFx6G/WpOB0+OO9aYeII4LQLSlTthuHh 0DZzUXhOR8bEMO1yTeV00+SvcaayEsXX6pLTOHinhJwu3Wfx3cYFQYNfUe/qL+8kVT7WtRFK kVS+yw0rKF0+lbDczXmdxixoXrBoRtFHtQNTqs17waCzqeS6AGcboQZctJfQIM6sOVnZWAH7 UKmksPHPARqm7yKan3Io994sgiOESQSKGYDYwoNQg0E/8TvrekPYvTnHocL/Emd3o2dJN3g/ 9yZhHNh2OhL3Kbnw43+rA+X2Wv9znTcZldtvl2/Y46z0u9uiGeYi2GA7FHa6bNfKd/cQATc+ ncDnMea4aYFCpTleM2xrAclQ+3BCxWtamW0bbtT838Jqm3FF5mLINk43d2GDB01WvvogBewC KMphStf5YVIIFyhZrJtboS6BqwClPa9Tom9Da2PNoMRMvCdkTNrGgk+NCZ8OEi9wCARfV0XZ P93jO73UCpHUPw5pNZIb7ZCjeBDKt8CKZP7HMinlXxLIJKRY3maTbptDbd9RrFR0U9wmy2Eo 753bpPUoz0GCbGWSnSJrOY7cA5bRVBmVcGeg5EGKoarf1s2cEl/UaO56e16IeRNwf8F/tokC 1nhMqOu4Aek2y2vxMTjQisLVY4Dqr4l8itgYXZ1bQn4s5XhCK72hJoim1IMVeFP3IReITRcF ZHpou2MXaZCTCrp4TMYYcWvpYBubk311w2JOCWhbTcleIN4XErC/dq9Jlnj8ywHDyyWs8oio uzwjViCGsVdGAkyXtzLbP+Pzk+quSRPkuxFWUaVcMJYf1/h8dQ3JiGo1q03LsgAJA/t3Dyf0 wrKUx4UqfOU+t0x/dzMnryJtcGlHrImTEZdGmDa65ewNDXbpzbyn9UfDbzQJT2EDTH64qSvY +lR3srQCvxfkQYYqZd4HpZq0bk6u4nlqYhcw1k2B37MdVmqVu5tL3TfhptPu6RBy6VjtBOyS 16I/tUGa7yFNNm8TgweIw0qaumMz/YJgiKU5vMweR2o6Chy9buBcENTIxjd2HcGdeAqbtwok bU7pcobyw2jkR52YNyIuSZZqjaXJXsaXqR765wXDdO5igcvzV0eM5XQBjWsu8OKYtRId1Yve 3qa2feEiLNbyU7PNXE0ECGVj+ZagJ0PvjFMzUMDdwvVwIub3qdv0U0D6ykzQyRU0g5Dj7B5N F9tOhAnPq6J5Tpp2JVOUjH+HwBaGCCf4VH7z1dVxmTVQ1P2Bj7IJWw5JeHf80ce/GZRcSJc4 amDjWPsVz/lcYKqgXtjBRM7+6O6FIIy6wvZhcq8FN6EFZQSbj3ijaujanAPtgP8R8g2gRSf9 +Vt+e9xb4z9NDIR8v1gUNDBiupPRUDWPnFGTNFg4LgNQTPWdga01GXcMEu2YM5Me6HH/EPkW cViKtgTBka+yDqWtWJcQqEWJKJsh7gm490Nfr6tLmkD9LSFqSdx947U/zD6mXRsWMhkis0nK 4ncej/eQHacg2BYxz3EoMVeYDHqZNAFYEjj2bnw/rhUUZ0Et+5ofAc51b7t5yeZNw5u/hS1u gLfZv+Jk7Yzl9w0x4a8QL9eAwiUKM/oULja+g6EtdkTP8jENt3Dtl9Ip1TqV+iM0WD9hziqe XWxXN/LMIftub83VyXGnsDEGfQUo8q1W+VTP4T8K3wyce5uniPzy0Nrxox6AcUhfBBhCg2PS Ay/Z8+9esQSRs9GgnZSbkCy1j4DXr/vYP6ISTyV9pyx59t07eADBNyg8nDtYG5BcTIQINv1D QqcVzNCIDxHhNwkOSLozM2Kz3O1zJEPlEfmmxDMWeGkM1SV
- Ironport-hdrordr: A9a23:XXcjAqy+OHX+zasRQMuUKrPxdOskLtp133Aq2lEZdPULSKDo7/ xGzc53pGbJYWgqMgBHpTnmAtj/fZq8z+8L3WB1B9iftWbdyRiVxe1ZnPffKnjbalnDHgA079 YhT0BRYOeATGSSzvyKrTVRKr4bsZe6GdmT9KTjJ8IHd3AhV0gf1XYPNu/rKDwGeOAcP+tzKH P03KMuzEvFCA9nE/hXHkN1JdQr5ee75q4OByR2TyLPxzPusdrC0s+LL/H35GZqb9uPqY1SlF QtUDaY2kxgiZ+GIq+27R6d032boqqD9jNPb/b8w/T82l7X+3CVjU1aKt/y2wwdkaWU8V4v1P PMrx0jM8k2y3SUUHqyvQKF4Xit7AoT
- Ironport-sdr: aVlzhPgdYjK8MA/x3/h7naZ7Icle3dEhKTF3J7fdGTVD/R3ZDZNc+Sb2youUiYxbiSUi+aNWrH 7eHbKyl4nmYExkJaRk6H1SV53ULdLTg/36f01WIbeQSZ8fxWwkd4Y2f4mxWptV6Ab3Oq86M67b p4/w2hyapC1XTMzTyuM1/b8kMbpgHsKDmTITMeBZzEkvrtYuv1OrPl2EYFIWTQjpCztN4jkwDh EBc9jap/3jS6LET7s7nYqkgxHoIF87F4Shm78xfpot/nUQwBiNn8yFVZDSaatTHYlLPFq6jLub UGvcdzmGdH2Ozt66NJ6ui5KO
- References: <cf66f27a-054f-4c3e-bc36-bb5463a99e49n@googlegroups.com>
Hi Dane,
it's `TC!TCConsistent` because TwoPhase instantiates TCommit under `TC` on line 163.
Markus
> On May 25, 2022, at 5:49 PM, Dane Hillard <dane.hillard@xxxxxxxxxx> wrote:
>
> In the video course, lecture 6, Leslie indicates to add an invariant to the model for the TwoPhase specification—namely, TCConsistent from the TCommit module. I have a specification open with TwoPhase as the root module, and as expected the toolbox is also showing the TCommit module because TwoPhase imports it. When I attempt to add the TCConsistent invariant, TLC indicates an error:
>
> Unknown operator: 'TCConsistent'
>
> I ran into this same limitation again in lecture 8 when attempting to add TCSpec as a property. I've attached a screenshot of my setup; the two modules contain exactly the content from the example repository, so perhaps I've done something else silly?
>
> Toolbox version: 1.7.1
> OS: macOS 12.2.1
> Java: openjdk 18
>
> <Screen Shot 2022-05-25 at 20.37.29.png>
--
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/232C41FB-8485-42BB-B909-9D0BD72D45F3%40lemmster.de.