[Date Prev][Date Next][Thread Prev][Thread Next][Date Index][Thread Index]
Re: [tlaplus] Re: understanding temporal properties
- From: Markus Kuppe <tlaplus-go...@xxxxxxxxxxx>
- Date: Sat, 6 Oct 2018 16:40:16 -0700
- Autocrypt: addr=mar...@xxxxxxxxx; prefer-encrypt=mutual; keydata= xsFNBFMlWsgBEADAFt/3gfTquM6dfOwSttLZYCoauipVYrLDFNwuWJllo7cJet4hGTAuyTLk du0+X/LM5KlqiYV6wXWWlRL0GMVidCn9WodjEt5atvxbC9Mn2qdAo+dWLOBBHbO4qh86eF7I H2yHzy1nIdJAyh7ibp9VtErsw7Zg8rudE05BkVVJGtqR10trnqZSEz9yw4GPwXPPK9IHP2Qp mfUdt93Z/tahZBJ6IhYVCVwS3Y6h1GlqwHsB+ifSeuX0Ye5pm1/iDD98z99jZSyl12biJE3U ZWL0UT1+BU0E7PxB+F2w3pdCPAuRANZ+9miFLbK9weBmhbHfDg3SfuxISePbQd2e+n1P2tde nnKRexME0509Yqc74zgApBe9uvVA1fTxH+CGn4w0kejNQItf8VMlmb8RxwxedMkyfpVo19H1 lxYJjvuFpV0GRZo61hK27/BNJlzUgT8RJqMObAVYqhQU4V9Q8bu1JI+kc4JkkLbzJIxnYhJ+ 0tD2CVxWX+/i8Tlchig0qRwftgbz4hJ0EsBK+88GKAPzJwIP7Vj8CeLOVKwtxn6qGAIRbBDN XjRuNA4KdcpjU+LIQoCPUeWdaD7gECkupAxsnf3N8WFFEhW3CHmc4C1IV6MVItYK1TauBQBx RoZdCkvKi2Gyx90HjG1uBnrgBP2OKL+shih6erAliZnq4KqtVwARAQABzSNtYXJrdXNAa3Vw cGUub3JnIDxtYXJrdXNAa3VwcGUub3JnPsLBfQQTAQgAJwUCWbO33gIbAwUJCWYBgAULCQgH AgYVCAkKCwIEFgIDAQIeAQIXgAAKCRBpnfZncqNjEwppEACIUkpPMXYXENA0agtC2biVAsKk ClBehl9d60MzVNoDDDqklH2tvX9VIEG1eHFEQVPHpuVyD4Qd87JpMvuQD5VByb0Erwbip/pr quqzir58ZctpgxzYw+EV4rH4tfCBQ8UNuXWono0kOPO73COl/iwy2L5mmuEvkhWqh9RJcnF3 oJvYaTS8jmQaHyhf/I1Ih/7LZr2ER7BC85URiKiZmGuREEVuUzv+H+LWSzdwIW72s8lyVxu1 xwgqVqBI/65Y5DXN3qD9L7jq/Q3uDXndAuoLQfnIk5KBthKFR9lcscBKPV7/f2TomDS5lc39 bdN+a0Bs2Ihqq2sVESrw0q3Wg/ziP7nDDYYKrtyDjThLhBVAifOUlln0kCCArl71t5ySoRbV mCeujpLWgOd3WNISn1njOj2qlO5NwDWg/NKzpO6VfzZULBIJ1UFLRuu7oZuFXtgl0b3I7V/4 nleNu2L6asxtP5FxLcC1wUHW8lPFpZ0twpnf1TnHl3a/1241xVywNl4BQbqH7fz2JFHK/ixj jgBzCYGGkq6RgmK5LIa1LVgxX56GWMPxQFgMWtOUaLFWHlHdLqp4u8ELr7vo6mxxjruJFSeD wTuOJehcj2ed7DnBv5KEXan/YeUv1+Uf4kyp9Hw4iilBWmLwvyqDl0c6rPxcc4iNooz9nGde Lr3eDkJno87BTQRTJVrIARAAlAyDS582RkWBM8tWcU/NEC6NBgicTUt8t7LsTTERxRGPmuRB uvgNU6f+PwfCpLxyQy2oKQHoyvIuxRkvVDNdcITcl4HU7/PZ+QEykjhlDWmzj2lFj99xrJNM 9L76+ZWCjKjcuZteZL/8XuG0Y2jRXQDWDSDwk9y1JQmwfFCAgNZZ2MhhA6HwxfLHV3RrsYBs BhJnYWsuFx0iRpFNxnXIzBG0sPj/3nu2Kn0yMFnIQIDzylfnKXbyPS+Ei6MlbZ70iEEoBiYy mkEpF94lat0sxIniqzD6SBp0JW5AinhuDCUSHYaDlkBr8pacvkrgQGVyJiQdiAw2dMGlxM5F W+PByt94psXVotbMj/riWvVT8u68lGyWIA1updUcb6Ty2uI31LywfS15s5NpEywu/A4p3eas 4iWGbjZCdB634Q+WDFjic2HF53E9UY8XTY0tb0cfjQivsH/n7YzFB13ylydgg/NxPwL6tBxe SBU/K71RCb2zyI7Cq5j6Df+DI4kwfSL0MtqIxL/BbJI7NgEJYcXWH+39o1r+8UMvZjUc7DSp GBvknWSmDKLex06CyrqfSwWHHsZEvB/8+0xl3fKQMK212x9Js/VsMSeh56/NW4gRfj06U8HP ErM0DOy0AfMt2eFlHYHLk5zedpqrpM7KQKMLKXUvDaw9JfVIgyENrqCXbU0AEQEAAcLBZQQY AQgADwUCUyVayAIbDAUJCWYBgAAKCRBpnfZncqNjExfUEACnlUGDdAOp+l7a2v7PL4tfVxor bpBjAQaETw0SEFw+v2BYtlGzn3iYSFc8B9VAx6QJdbROGAtVt0uu4MRUnhu+5GbQ5ZKED7J1 uMw62e2KDWp20tHX7FPsywQURiTBh0guKrujms7P6RfNPouI2teV19arIxV7yJM9D8Q3/oBL iR2kBnHZI+SD2A4vX9153KJUgb+CjhX3RVnfzrG97f8NIr4x27isaknwHb/7xOqoslxsDR+k pfaBclfGHKm2ONzLieOzk7vtnXdA17ZWpoCb3ep288XdHsmwTO+1COogWoKzkS89SNCExY1u rfyczE2JaFFbPIHJzGMBsT4KRQpt3mOL2Ohfkhz/shykuAb5r4h5uF+fP9LOiGbt7edmwP1c zfdKjmj3zMCufU6WUsYr96mGMgeOQ2f53xXyFyLOdqH3YFdwvpzyg8D/E1BqJff5xS20hEs5 mEQ0qDdCD2JiVfA2l0IVisieFiZwQVYg32+PZLdsigj3qjuyD0K2Y+63R/ifn6ZfdQ9T2Yx2 KnqUolYMtO5mEEJ84KdaXsaUGWaq/Xy7ozXR8Km4nG4NycPEGB/KPkQmcqxhF82Zcic+hbxe VOd8SIyzgWAMZI4MaHF1ElpB7ribzSpEEUc5yt2XlD83SuU6EGIGetJSlTwLY6tsWIdopfUs KBtGovE4Xw==
- Openpgp: preference=signencrypt
- References: <aff08298-1b11-4bc7-a8b1-5ca0c61148f9@googlegroups.com> <da1e1b81-e4f5-4aa2-a6f1-d87211f5a0a0@googlegroups.com> <CAH4a_VVmQE3jE=fGDTVpRrQR8uapxv86jqCDDWV3pjmwUyKyiA@mail.gmail.com>
On 05.10.2018 17:08, Bekir Oguz wrote:
> Is there a way to ask the model checker to give all paths in which the
> invariable is falsifiable instead of stopping at the first failure?
Hi Bekir,
you can run TLC from the command-line with the "-continue" parameter [1]
which causes it to print error traces but keep exploring. This is not
supported from inside the Toolbox though [2].
Thanks
Markus
[1]
https://github.com/tlaplus/tlaplus/blob/f4763d800472fd3f5c4ce1913ee01cf46bf2a6d4/tlatools/src/tlc2/TLC.java#L138-L201
[2] https://github.com/tlaplus/tlaplus/issues/79