how can I assert that a number goes or a list grows up in TLA+?





.everyoneloves__top-leaderboard:empty,.everyoneloves__mid-leaderboard:empty,.everyoneloves__bot-mid-leaderboard:empty{ height:90px;width:728px;box-sizing:border-box;
}







2















I have a TLA+ spec where I would like to assert that a list only ever grows in length (it's fine if it stays the same when stuttering.)



Right now I have something like this, but I'm certain that it's not right:



NoWorkIsLost == Len(samples) = Len(samples) ~> Len(samples) = Len(samples) + 1


I'm not even sure what to search for here, I'm sure I'm missing something super obvious!






tla+







share|improve this question





























    2















    I have a TLA+ spec where I would like to assert that a list only ever grows in length (it's fine if it stays the same when stuttering.)



    Right now I have something like this, but I'm certain that it's not right:



    NoWorkIsLost == Len(samples) = Len(samples) ~> Len(samples) = Len(samples) + 1


    I'm not even sure what to search for here, I'm sure I'm missing something super obvious!






    tla+







    share|improve this question

























      2












      2








      2








      I have a TLA+ spec where I would like to assert that a list only ever grows in length (it's fine if it stays the same when stuttering.)



      Right now I have something like this, but I'm certain that it's not right:



      NoWorkIsLost == Len(samples) = Len(samples) ~> Len(samples) = Len(samples) + 1


      I'm not even sure what to search for here, I'm sure I'm missing something super obvious!






      tla+







      share|improve this question














      I have a TLA+ spec where I would like to assert that a list only ever grows in length (it's fine if it stays the same when stuttering.)



      Right now I have something like this, but I'm certain that it's not right:



      NoWorkIsLost == Len(samples) = Len(samples) ~> Len(samples) = Len(samples) + 1


      I'm not even sure what to search for here, I'm sure I'm missing something super obvious!






      tla+




      tla+






      share|improve this question













      share|improve this question











      share|improve this question




      share|improve this question










      asked Jan 3 at 20:54









      Brian HicksBrian Hicks

      3,21264269




      3,21264269
























          1 Answer
          1






          active

          oldest

          votes


















          2














          It depends on what you mean by "the list only ever grows in length". The simplest way to do that would be to write



          Op == [Len(samples') > Len(samples)]_Len(samples)


          But that's saying that if the length changes, the length must increase. That still allows for you to mutate the list without changing it! If you instead write



          Op == [Len(samples') > Len(samples)]_samples


          Then you are saying that if samples changes, it must also increase in length. But this allows you to pop one element and push two in a single action. You probably want to express that the old sequence is a prefix of the new one. You can do that with



          Op == [SubSeq(samples', 1, Len(samples)) = samples]_samples





          share|improve this answer
























            Your Answer






            StackExchange.ifUsing("editor", function () {
            StackExchange.using("externalEditor", function () {
            StackExchange.using("snippets", function () {
            StackExchange.snippets.init();
            });
            });
            }, "code-snippets");

            StackExchange.ready(function() {
            var channelOptions = {
            tags: "".split(" "),
            id: "1"
            };
            initTagRenderer("".split(" "), "".split(" "), channelOptions);

            StackExchange.using("externalEditor", function() {
            // Have to fire editor after snippets, if snippets enabled
            if (StackExchange.settings.snippets.snippetsEnabled) {
            StackExchange.using("snippets", function() {
            createEditor();
            });
            }
            else {
            createEditor();
            }
            });

            function createEditor() {
            StackExchange.prepareEditor({
            heartbeatType: 'answer',
            autoActivateHeartbeat: false,
            convertImagesToLinks: true,
            noModals: true,
            showLowRepImageUploadWarning: true,
            reputationToPostImages: 10,
            bindNavPrevention: true,
            postfix: "",
            imageUploader: {
            brandingHtml: "Powered by u003ca class="icon-imgur-white" href="https://imgur.com/"u003eu003c/au003e",
            contentPolicyHtml: "User contributions licensed under u003ca href="https://creativecommons.org/licenses/by-sa/3.0/"u003ecc by-sa 3.0 with attribution requiredu003c/au003e u003ca href="https://stackoverflow.com/legal/content-policy"u003e(content policy)u003c/au003e",
            allowUrls: true
            },
            onDemand: true,
            discardSelector: ".discard-answer"
            ,immediatelyShowMarkdownHelp:true
            });


            }
            });














            draft saved

            draft discarded


















            StackExchange.ready(
            function () {
            StackExchange.openid.initPostLogin('.new-post-login', 'https%3a%2f%2fstackoverflow.com%2fquestions%2f54029656%2fhow-can-i-assert-that-a-number-goes-or-a-list-grows-up-in-tla%23new-answer', 'question_page');
            }
            );

            Post as a guest















            Required, but never shown

























            1 Answer
            1






            active

            oldest

            votes








            1 Answer
            1






            active

            oldest

            votes









            active

            oldest

            votes






            active

            oldest

            votes









            2














            It depends on what you mean by "the list only ever grows in length". The simplest way to do that would be to write



            Op == [Len(samples') > Len(samples)]_Len(samples)


            But that's saying that if the length changes, the length must increase. That still allows for you to mutate the list without changing it! If you instead write



            Op == [Len(samples') > Len(samples)]_samples


            Then you are saying that if samples changes, it must also increase in length. But this allows you to pop one element and push two in a single action. You probably want to express that the old sequence is a prefix of the new one. You can do that with



            Op == [SubSeq(samples', 1, Len(samples)) = samples]_samples





            share|improve this answer




























              2














              It depends on what you mean by "the list only ever grows in length". The simplest way to do that would be to write



              Op == [Len(samples') > Len(samples)]_Len(samples)


              But that's saying that if the length changes, the length must increase. That still allows for you to mutate the list without changing it! If you instead write



              Op == [Len(samples') > Len(samples)]_samples


              Then you are saying that if samples changes, it must also increase in length. But this allows you to pop one element and push two in a single action. You probably want to express that the old sequence is a prefix of the new one. You can do that with



              Op == [SubSeq(samples', 1, Len(samples)) = samples]_samples





              share|improve this answer


























                2












                2








                2







                It depends on what you mean by "the list only ever grows in length". The simplest way to do that would be to write



                Op == [Len(samples') > Len(samples)]_Len(samples)


                But that's saying that if the length changes, the length must increase. That still allows for you to mutate the list without changing it! If you instead write



                Op == [Len(samples') > Len(samples)]_samples


                Then you are saying that if samples changes, it must also increase in length. But this allows you to pop one element and push two in a single action. You probably want to express that the old sequence is a prefix of the new one. You can do that with



                Op == [SubSeq(samples', 1, Len(samples)) = samples]_samples





                share|improve this answer













                It depends on what you mean by "the list only ever grows in length". The simplest way to do that would be to write



                Op == [Len(samples') > Len(samples)]_Len(samples)


                But that's saying that if the length changes, the length must increase. That still allows for you to mutate the list without changing it! If you instead write



                Op == [Len(samples') > Len(samples)]_samples


                Then you are saying that if samples changes, it must also increase in length. But this allows you to pop one element and push two in a single action. You probably want to express that the old sequence is a prefix of the new one. You can do that with



                Op == [SubSeq(samples', 1, Len(samples)) = samples]_samples






                share|improve this answer












                share|improve this answer



                share|improve this answer










                answered Jan 7 at 3:03









                HovercouchHovercouch

                93578




                93578
































                    draft saved

                    draft discarded




















































                    Thanks for contributing an answer to Stack Overflow!


                    • Please be sure to answer the question. Provide details and share your research!

                    But avoid …



                    • Asking for help, clarification, or responding to other answers.

                    • Making statements based on opinion; back them up with references or personal experience.


                    To learn more, see our tips on writing great answers.




                    draft saved


                    draft discarded














                    StackExchange.ready(
                    function () {
                    StackExchange.openid.initPostLogin('.new-post-login', 'https%3a%2f%2fstackoverflow.com%2fquestions%2f54029656%2fhow-can-i-assert-that-a-number-goes-or-a-list-grows-up-in-tla%23new-answer', 'question_page');
                    }
                    );

                    Post as a guest















                    Required, but never shown





















































                    Required, but never shown














                    Required, but never shown












                    Required, but never shown







                    Required, but never shown

































                    Required, but never shown














                    Required, but never shown












                    Required, but never shown







                    Required, but never shown







                    -

                    Popular posts from this blog

                    Monofisismo

                    Image
                    Monofisismo (do grego: monos - "único, singular" e physis - "natureza") é o ponto de vista cristológico que defende que, depois da união do divino e do humano na encarnação histórica, Jesus Cristo, como encarnação do Filho ou Verbo ( Logos ) de Deus, teria apenas uma única "natureza", a divina, e não uma síntese de ambas. O monofisismo é contraposto pelo diofisismo (ou "diafisismo"), que defende que Jesus preservou em si as duas naturezas. Historicamente, o monofisismo se refere primordialmente à posição dos que (especialmente no Egito e, em menor grau, na Síria) rejeitaram as decisões do Concílio de Calcedônia em 451 (o quarto concílio ecumênico). Os membros mais moderados entre eles, porém, defendem a teologia "miafisita", que se tornou a oficial para as Igrejas Ortodoxas Orientais. Muitos ortodoxos orientais, porém, rejeitam essa classificação, mesmo como um termo genérico, mas ele é amplamente utilizado na literatura históri
                    Read more

                    Angular Downloading a file using contenturl with Basic Authentication

                    Image
                    0 I have a contentUrl when user clicks on that,file should be downloaded. If I try to browse the contentUrl in the browser it asks for Userid and password.I believe this is Basic Authentication.I dont want user to enter UserId and Password so I am passing it Authorization(Please see below code). Url looks some thing like this: http://XXX.XXX.XX.XXX:8080/flowable-rest/service/runtime/tasks/90875/attachments/90555/content let username : string = 'admin'; let pwd : string = 'test'; let headers = new Headers(); headers.set('Accept', 'text/json'); headers.append('Content-Type', 'application/json'); headers.set('Access-Control-Allow-Origin', '*'); headers.set('Access-Control-Allow-Methods','POST, GET, OPTIONS, PUT, DELETE'); head
                    Read more

                    Olmecas

                    Image
                    Monumento 1, uma das quatro cabeças colossais encontradas em La Venta, com altura aproximada de 3 metros Olmecas é a designação do povo e da civilização que estiveram na origem da antiga cultura pré-colombiana da Mesoamérica e que se desenvolveram nas regiões tropicais do centro-sul do atual México durante o pré-clássico, próximo de onde hoje estão localizados os estados mexicanos de Veracruz e Tabasco, no Istmo de Tehuantepec, numa zona designada área nuclear olmeca. A cultura olmeca floresceu nesta região aproximadamente entre 1500 e 400 a.C., [ 1 ] e crê-se que tenha sido a civilização-mãe de todas as civilizações mesoamericanas que se desenvolveram posteriormente. [ 2 ] No entanto, desconhece-se a sua exacta filiação étnica, ainda que existam numerosas hipóteses colocadas para tentar resolver esta questão. O etnónimo olmeca foi cunhado pelos arqueólogos do século XX, e não devem confundir-se com os muito posteriores olmecas-xicalancas que ocuparam vários locais do México
                    Read more