Tau Language REPL Syntax

[S1r_4zdr3w(OP)]

Hi guys, any idea why when normalizing these formula, one gave me a result of 1 and the other gave me a result of T. My guess is that the first formula Tau treat it as BA formula while the second formula, Tau treat it as Tau formula. Am I correct or missing something?

[S1r_4zdr3w(OP)]

Tau Formula:

tau => "(" tau "&&" tau ")" | "!" tau | "(" tau "^" tau ")" | "(" tau "||" tau ")"
    | "(" tau "->" tau ")" | "(" tau "<->" tau ")" | "(" tau "?" tau ":" tau ")"
    | "(" term "=" term ")" | "(" term "!=" term ")" | "("term "<" term")"
    | "("term "!<" term")"    | "(" term "<=" term ")" | "(" term "!<=" term ")"
    | "(" term ">" term ")"    | "(" term "!>" term ")" | "all" var tau
    | "ex" var tau | tau_ref | T | F.

Boolean Functions:

term => "("term "&" term")" | term "'" | "("term "+" term")" | "("term "|" term")"
    | term_ref | constant | uninterpreted_constant | var | "0" | "1".


So this explains why the first formula gives 1 while the 2nd formula gives T. This is because Tau sees the 1st formula to be a Boolean Function while the 2nd formula to be Tau Formula.

[Lucca Tiemens]

Hi S1r_4zdr3w,

your conclusion is correct. The first one is a Boolean function which is passed to the normalizer while the second one is a Tau formula.

Best,
Lucca

[S1r_4zdr3w(OP)]

Hi Lucca,

Thank you for your response. A follow up question.

Q1: is it possible to stop Tau from running? just curious.

For example I did the example o1[t] = 0, I run it and then Tau ask me, "no inputs vars defined, how many steps do you want to perform?" I put a large number for testing (10,000) and its not stopping till it reach that number, it's actually amazing to see it run.  Is there a key I can type to stop it?

Q2: Also, does the result stored in my computer or if I entered cleared, it will remove everything?

Thanks!

[pk]

Q1: is it possible to stop Tau from running? just curious.

For example I did the example o1[t] = 0, I run it and then Tau ask me, "no inputs vars defined, how many steps do you want to perform?" I put a large number for testing (10,000) and its not stopping till it reach that number, it's actually amazing to see it run.  Is there a key I can type to stop it?

Q2: Also, does the result stored in my computer or if I entered cleared, it will remove everything?

Thanks!

A1: If you compile an up to date version from Github, there is a new mechanism of execution that goes through steps one by one. One can stop the execution by pressing q followed by enter, otherwise pressing the enter key on its own continues to the next step.

A2: If you declared your output variable, say o1, to the standard output i.e. 'sbf o1 = console' then it won't store the results.
But results can easily be stored in a text file by changing that output variable declaration into 'sbf o1 = ofile("my_output1.txt")' for instance.
One can also store the output in a different location by providing a full path like: 'sbf o1=("/tmp/tmp_tau1.out")' so the output from o1 goes to /tmp in this example, instead of the tau executable location.

[S1r_4zdr3w(OP)]

Thanks pk!

I tried to compare windows OS Tau executable and Ubuntu Linux OS Tau build-Release.

Without declaring my input,

1. In the Tau executable, it ask me how many steps do I want to perform the program. Then it will run depending on the number of steps I gave.
 
2. In the Tau build-Release, it will run the program step by step. And it will only stop when I type q for quit.

What I think I learned:

1. In Tau executable, it will ask how many times I want to run the program. It's like more into execution. It will run the program in one go from start to finish.

2. In build-Release, it will not ask how many times I want to run the program. So I may test it by providing different scenarios to see the program's reaction. The program will run step-by-step and that's why I can just write "q" to quit the program.

I also tried your code recommendation of storing the results. Since I was running the code on the folder build-Release, that's where the .txt was saved. And yes, I can find all the results there. Thanks for the great info!

Here is my comparison of the two. In the build-Release, we need to save the output at .txt to see the result


http://youtube.com/post/UgkxkSJ6fL25NdUUwTqJOzJkRpDz-fCjReTf?si=mKQl5Qv0AWMpa-G3