Here you can ask questions and find or give answers to organizational, academic and other questions about studying computer science.

1.1k questions

1.2k answers

1.6k comments

538 users

0 votes

Please find below my solution is which is different from the exam solution:

Justification for S1 with signal traces

a                   | (1)ω

Fa                 | (1)ω

Xa                | (1)ω

[Fa SB (Xa)]  | (1)ω        {because eventually "a" holds (which is from the first point of time)  before next of "a" (as next of "a" is true: self loop) and eventually "a" holds forever (self loop)}

Justification for Swith signal traces

a                   | (1)ω

¬Xa              | (0)ω

(a & ¬Xa)    | (0)ω

F(a & ¬Xa)  | (0)ω

Please let me know if my solution is also correct or I did any mistake?

In general can there be multiple solutions to these kind of questions?

Thank you in advance.

in * TF "Emb. Sys. and Rob." by (370 points)
edited by

1 Answer

+1 vote
 
Best answer
[p SB q] demands that p holds before q holds, so if p is 1^omega and q is 1^omega, then [p SB q] is 0^omega which is then the same as F(a&!Xa) on your path. Hence, your solution is wrong.
by (166k points)
selected by
Thank you for the clarification.

Related questions

0 votes
1 answer
asked Aug 24, 2020 in * TF "Emb. Sys. and Rob." by nikita (300 points)
0 votes
1 answer
asked Aug 23, 2020 in * TF "Emb. Sys. and Rob." by ssripa (550 points)
0 votes
1 answer
asked Aug 20, 2020 in * TF "Emb. Sys. and Rob." by nikita (300 points)
0 votes
1 answer
asked Aug 20, 2020 in * TF "Emb. Sys. and Rob." by maherin (370 points)
0 votes
1 answer
asked Aug 9, 2021 in * TF "Intelligent Systems" by RS (770 points)
Imprint | Privacy Policy
...