Global Model Checking (exercise sheet 6 question 3)

Question

This is my solution but it's not correct. Could you please tell me what part is wrong?

Answer 1

wow! This solution is well-structured and almost perfectly correct. You just forgot to add s₁ for the second []x. Great work!

Answer 2

Yes, good work that just has an unfortunate error at the end (as Martin wrote []x yields {s1} so that the final []x|y should be {s0;s1;s2;s5}).

You can check where you go wrong with the teaching tool https://es.cs.uni-kl.de/tools/teaching/ModelChecking.html where you need the following input in your case

    vars a,b;
    init 5,6;
    labels 0:a; 1:b; 2:a; 3:a; 4:; 5:a; 6:; 7:b; 
    transitions 0->4; 0->5; 2->0; 3->4; 4->0; 4->3; 4->4; 4->6; 4->7; 5->0; 6->4; 7->4;

and

        mu x.([]x | nu y.(a&a&<>y))

Then, you will get the following output that you can compare with your results:

 computing states of mu x:bool. ([] x | nu y:bool. (a & a & <> y))

    step 0 : x = {}

        〖x〗= {}

        〖[] x〗 = {s1}

        computing states of nu y:bool. (a & a & <> y)

            step 0 : y = {s0;s1;s2;s3;s4;s5;s6;s7}

                〖a〗= {s0;s2;s3;s5}

                〖a & a〗 = {s0;s2;s3;s5}

                〖y〗= {s0;s1;s2;s3;s4;s5;s6;s7}

                〖<> y〗 = {s0;s2;s3;s4;s5;s6;s7}

                〖a & a & <> y〗 = {s0;s2;s3;s5}

            step 1 : y = {s0;s2;s3;s5}

                〖y〗= {s0;s2;s3;s5}

                〖<> y〗 = {s0;s2;s4;s5}

                〖a & a & <> y〗 = {s0;s2;s5}

            step 2 : y = {s0;s2;s5}

                〖y〗= {s0;s2;s5}

                〖<> y〗 = {s0;s2;s4;s5}

                〖a & a & <> y〗 = {s0;s2;s5}

                〖y〗= {s0;s2;s5}

        fixpoint reached!

       〖nu y:bool. (a & a & <> y)〗 = {s0;s2;s5}

       〖[] x | nu y:bool. (a & a & <> y)〗 = {s0;s1;s2;s5}

    step 1 : x = {s0;s1;s2;s5}

        〖x〗= {s0;s1;s2;s5}

        〖[] x〗 = {s1;s2;s5}

        〖[] x | nu y:bool. (a & a & <> y)〗 = {s0;s1;s2;s5}

        〖x〗= {s0;s1;s2;s5}

    fixpoint reached!

    〖mu x:bool. ([] x | nu y:bool. (a & a & <> y))〗 = {s0;s1;s2;s5}