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?
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.
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
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!
Quote from: S1r_4zdr3w on Dec 13, 2024, 10:17 AMQ1: 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.
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=Xy6PiGKfiL1PAwfY)
http://youtube.com/post/UgkxkSJ6fL25NdUUwTqJOzJkRpDz-fCjReTf?si=mKQl5Qv0AWMpa-G3