[Date Prev][Date Next][Thread Prev][Thread Next][Date Index][Thread Index]
Re: [tlaplus] TLA+ Toolbox issues?
- From: Markus Kuppe <tlaplus-google-group@xxxxxxxxxxx>
- Date: Sun, 8 May 2022 10:58:56 -0700
- Ironport-data: A9a23:tB/vq6CgrOcWfBVW/9Lmw5YqxClBgxIJ4kV8jS/XYbTApGgi0zcHn 2QZXW/QO/3bMGOkfNB/Ooy0pENSuJ6Ex95lOVdlrnsFo1Bi+ZOUX4zBRqvTF3rPdZObFBoPA +E2MISowBUcFyeEzvuVGuG96yE6j8lkf5KkYAL+EnkZqTRMFWFw0HqPp8Zj2tQy2YXhU1vU0 T/Pi5S31GGNi2Yc3l08sPrrRCNH5JwebxtF1rCWTakjUG72zxH5PrpHTU2CByeQrr1vIwKPb 72rIIdVUY/u10xF5tuNyt4Xe6CRK1LYFVDmZnF+A8BOjvXez8A/+v5TCRYSVatYozrXsflwk tRMj7ahezkKBvH+kb8RVBYNRkmSPYUekFPGCX22sMjW0EifNnWym7NhC0Y5OYBe8eFyaY1M3 aZAeXZdM1ba3bLwnurTpupE3qzPKOH3OIoHvmx7jjvfBtwNYaL7bJXm1fZx5h1qq+ISNtTnQ uUgRBcwQSXwSDxnNVAQB5Yzk/2vm2HkNTZfrTp5oIJuuDWLll0gidABNvKOKtyDePt0hH2l/ D72r373BDAjJs2QnG/tHnWE37eTx0sXQrk6GLyj/eNxm3WPwmVVDQYMEFq9u/iwzE+4QdNWb UIOkhfCtoA3/U2vC8b4Bli2/ibCsRkbVN5dVeY97Wlh15Y4/S6WWEYtT2RAaeYMpf0IZgR25 FbSk9TmUGkHXKKudVqR8bKdrDWXMCcTLHMfaSJscefjy4mzyG3UpkKfJuuPAJJZnfWuRm6tm 2HiQDwWwuRM3ZRShs1X6Hie22r0zqUlWDLZ8ek+Y45IxgZwZYrgeInxrFaFtbBPK4GWSlTHt 38B8yR/0AzsJc7R/MBuaL9VdF1M2xpjGGCF6bKIN8R7nwlBA1b5IehtDMhWfS+FyPosdz7ze 1P0sghM/pJVN3bCRfYpPtvhVJ9wkfKxSY2NuhXogjxmMsgZmOivrHEGWKJs9z2FfLUEyvxgY cjDL65A815DU/s/k1JauNvxIZdynnxkrY8ibZ/8yBuj3NKjiI29GN843K+1RrFphIvd+Fu92 48GZ6OilksCOMWjPHi/2dNDfDgicClnbbir+pw/XrDZfmJORjp7Y9ePmuNJRmCQt/g9ehHgo yrjCie1CTPX3hX6FOl9Qi09OO63AcYj/BrW/0UEZD6V5pTqWq73hI93Snf9VeBPGDVLwaEmQ v8bVd+HB/gTGD3L9y5EM8vyq4ttcBmknwWTJzHjaz86JsYySwvM897iXw3u6ChfXnHs7JBh/ eKthlHBXJ4OZwV+F8KKOvih+FW84CoGk+VoUkqUf9ReIR2+8IVjJyHroOUwJsUAdUfKyjeAj l/EBRodoPLRrpVz/NSQ3fKIqIKgEu1fGEtGHjCHvOjsanSApjKumNYSXvyJcDbRUHLP1J+jP egFnevhNPAnnUpRt9YuGbhcy69jtcDkoKVXz1g5EXjGNg/5Cr5pLnSc58RXsrxRwbtV5Vm/V k6Vo4cINrKON8foH0QWORI+KO+E0KhMyDXV6P00JmT85TN2rercChwJYEfThXwPNqZxPaMk3 fwl5Jwc5Tu5h0d4Kd2BlC1VqzmBI3FcAaUqspYWXN3ihgYxkAoQZJXdDmrp5cjKZYsUdEYtJ TCQiezJgLEFnhjOdH86FH7s2+tBhMRR5Eobkgdaf1nZyMDYgvIX3QFK9WhlRApiyBgagfl4P XJmNhEoKKjfrTNpn9R+WXuxEQVNWE+Q9kDrlQtbkWTYS1WvBGPKK2I5NOmX+10B6CdZdz5S8 7zbkzm1AGq3IpGuh3JsGlNjsOHpVtdr9wfPsM+gGMuBEpYgZif9memlYm9R80nrBsY4hUvmo +h2/bcgMvaibnFO/KBrWZOH0bkwSQyfIDAQS/9W+q5UT3rXfyu/2GTTJk29JpFEK/DQrR7qC 9ByPtkdEFOxziGTtitdCqkLLLt52vUu4Z0NYLT2PSkat7KHqidy94nN/DP1nm4hTthjzZQnJ oXKe27QG2CcnyEPyWrErc0BJW/hJNdaPEvz2+e69OhPHJUG6bk+fUY327qynnOULAo3oE7O7 V2bP/fbn7541IBhv4rwCaEfVQ+6HtX+CbaT+wepvtUSMN7CPK8ibe/ORoUL4uiXAVcQZzizv bGEsdqyw0ac+bhoCybWnJ6OE6QP7sK3NAaS3gQbM1EC9RZumue1i/fAx4x8AZNOl9xZ68a9Q Bagc427ctt9txJ12ihOcyYHe/oCI/2fU0ojzB9Ra9yDDR8S1QHINtS67WSvZmZeHsPN11sSF Ses08uTChtkQEigyfPK6zyKw3O1HbM7ZZYbSg==
- Ironport-hdrordr: A9a23:oooa5aog3Fqdt0O+QmxlYTsaV5tzL9V00zEX/kB9WHVpm5Oj+7 HXoB1L73KE8Qr5BktL6La90c67MA3hHP9OkPYs1NKZMzUO11HYX72KgbGSvwEIXheOgtK0O8 9bAuhD4POZNyk6sS+42nj0Lz4YqOP3vpxA/N2ujEuE+GpRGutdBnlCe3Gm+zxNNXh77MECZd GhD6N8zlLKCBBnFbXHOpQcZZm4mzSIruOVXfdhPW9u1OCgt1KVAdXBYmilN3klIkZyKXZLyx mhr+U73MWeWjOApCM1ZwTonttrcRfau7h+7MHmsLldFt0d4TzYEriJkofy3kFTnMifrGwymN 2JiRYtNcZ+5jfweSWauh3wwmDboXoT10M=
- Ironport-sdr: cjeQRo+NaBW4T3KFfXX81K27L96/qsAbgPxf7pviWMO+J2LiOrZ+TdVC/GOUNehNDtC3qgTHls p4sNFKE4ASVuxds/nCUJdvcC0a/4KRAoCMFNFh0hhNzzWD0NTkITLgs5/APjaWiAn3scIo/22E RIabskgG3WGtTLA+fz1mq+jf+mtNE1BxH/kMypGti8f8VqnkJrPKo39uoPHQPjy6aOR6VF/6Lo +MRrjYXRv1cU7OSmD7ItPLKpqErGdDGYmLbzNTMikt1GZKjwaQ5zhZImiHmk+Me2pQyCpM5FsU adVrnwFghTsUU4NxsgHZzdeq
- References: <67b2b3d6-0595-4fcc-9a78-2a5ff0f384c7n@googlegroups.com>
Hi Jones,
the Toolbox saves its settings in your user director in the '.tlaplus/' folder. The Toolbox does *not* use 'tla2tools.jar' but the classes in 'plugins/org.lamport.tlatools_1.0.0.202204200054' relative to the Toolbox installation directory. However, the classes should be the same.
Is it possible that the Toolbox model has 'Init' and 'Next' under "What is the behavior spec?" on the "Model Overview" page? At the same time, do you check 'SPECIFICATION Spec' on the command line? If that is not the case, let's move the discussion to 'https://github.com/tlaplus/tlaplus/issues’;.
Markus
> On May 7, 2022, at 4:49 PM, Jones Martins <jonesmvc@xxxxxxxxx> wrote:
>
> Hi everyone,
>
> In summary:
>
> • Where does the Toolbox save its settings?
> • Does the Toolbox run tla2tools.jar from /opt/TLA+Toolbox/tla2tools.jar?
>
>
> I’m running Ubuntu 22.04 and I’m having some issues with the Toolbox.
>
> I stumbled upon a liveness “bug” in the Toolbox version 1.71 and version 1.80, where TLC detects stuttering where there isn’t any when verifying liveness properties.
>
> The specification is simple enough to see there isn’t stuttering at all. I ran an external tla2tools.jar version 2.18 from the terminal and no problems were detected in my spec.
>
> So I thought: “Maybe it’s TLC. I should replace this tla2tools file with the one TLA+ Toolbox uses.” It didn’t work.
>
> Am I missing something?
>
> I’d like to do a clean install this time. A full uninstallation doesn’t seem to happen through sudo apt purge tla+toolbox because, when reinstalling the Toolbox through a .deb file, it seems to remember all my previous settings. Shouldn’t the settings be removed along the Toolbox when uninstalling?
>
> I hope this isn't confusing…
>
> Best,
>
> Jones
--
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/26F1F898-EF96-4419-B4E2-4577DFE01631%40lemmster.de.