[Date Prev][Date Next][Thread Prev][Thread Next][Date Index][Thread Index]

Re: [tlaplus] Pluscal Print



Dear Piyush,

1. The output that appears in the User Output panel is generated by TLC during its exploration of the state space. Since TLC does a breadth-first evaluation, the order in which print statements are executed may not be obvious, and it does not correspond to the execution order of individual runs of the algorithm. Moreover, whenever TLC encounters a state that it has already seen previously, it will not explore the successors of that state. That’s why you get fewer outputs than inputs: e.g., gcd(24,3) = gcd(24,9) = 3, so the result 3 is printed only once.

2. A string value in TLC consists of a sequence of characters enclosed in double quotes, so the way strings are printed by TLC is as expected (although it may not look particularly pretty).

Hope this helps,
Stephan


On 06 Jul 2015, at 08:50, Piyush Bansal <bansal....@xxxxxxxxx> wrote:

Hi,

Have few doubts regarding the pluscal print statement. For the purpose illustration I an using the following example:

--algorithm EuclidAlgo {
    variable u = 24; v \in 1..N;
    {
        print << u, v >>;
        while(u # 0) {
            if(u < v) { u := v || v := u };
            u := u-v;
        };
        print <<" Have GCD = ", v >>;
    }
}

While setting the value of N = 10, I got the following output 

<<24, 1>>
<<24, 3>>
<<24, 4>>
<<24, 5>>
<<24, 2>>
<<24, 6>>
<<24, 7>>
<<24, 8>>
<<24, 9>>
<<24, 10>>
<<" Have GCD = ", 8>>
<<" Have GCD = ", 6>>
<<" Have GCD = ", 3>>
<<" Have GCD = ", 4>>
<<" Have GCD = ", 2>>
<<" Have GCD = ", 1>>

I have two questions:
1) Sequence in which the two print statement works. Not able to match the input to the output. Moreover there is a mismatch in the number of input's, i.e <<u, v>> and expected output <<" Have GCD = ", v>>.
2) In case of second print statement, quotes used to represent a string were also printed on the console.

please clarify.

Regards,
Piyush



--
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+u...@xxxxxxxxxxxxxxxx.
To post to this group, send email to tla...@xxxxxxxxxxxxxxxx.
Visit this group at http://groups.google.com/group/tlaplus.
For more options, visit https://groups.google.com/d/optout.