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

531 users

Most popular tags

vrs vrs_exam vrs_exercise ltl ctl exam dira omega_automata rosy parallel_computing ltl_model_checking mbes processor_architecture zielonka se1 lo2 automata bdd mu-calculus sequent-calculus simplex temporal local-model-checking kripke studiengang_reform rosy_exam zdd2fdd vrs_lecture greatest-simulation bdd2fdd exists-algorithm fourier_motzkin equivalance bdd2zdd tool studiengangswechsel fdd2bdd floating_point_arithmetic snf induction simulation zdd curriculum_change symbolic_computation fdd2zdd ctl_model_checking predicate_logic dynamic_scheduling cmd b_complement_multiplication constrain-algorithm compose-algorithm #parallel_computing minic i2sc format robdd breakpoint acceptance curriculum_update basic_block_scheduling unit-tests finroc sche ddd2zdd zdd2bdd vrs_cheatsheet hrs infinite_path branch-bound pre-requisite thesis functional state-machine uml-diagram embedded-system ml1 registration pipeline_conflicts vector_computers actiontable modulo_scheduling static_scheduling organisation lo1 conditional #pram restrict ite programming compiler abacus scheduling parallel forall notation shannon important predecessors fdd

Categories

Clarification - Constrain

0 votes

I needed a clarification regards solution for constraint algorithm.

For the function call Constrain(β3, Φ3),  I think that the result should be Constrain(β5, Φ3). However in the solution sheet I see it is solved as "b-> Constrain(1,Φ3)| Constrain(β5,Φ3 ) " .

β3 has only one Leaf node and β5 is not a leaf node. hence the condition Constrain( β_0,Φ) must be invoked which is Constrain( β_5,Φ_3). If this is solved in this manner, in the final solution "b" will never exist. However if we solve as per it is solved in solution sheet "b" exists in the final answer.

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

1 Answer

+1 vote
 
Best answer
Why do you think so? Both the algorithm as well as the rewrite rules given on the slides are consistent with the example solution as far as I can see.
by (166k points)
selected by
The confusion to me was caused by treating BDD(0) as "leaf node" in general. It seems that BDD(0) stands for false leaf node and BDD(1) stands for True leaf node. Now I understood it clearly and I am now convinced with solution sheet answer.
by (1k points)
Yes, the Contrain algorithm reacts differently to BDD(0) and BDD(1) since one means that we are in the care set while the other does not.
by (166k points)
Yes, I now get it. Thank you for clarifying.
by (1k points)

Related questions

0 votes
1 answer
Mu Calculus - clarification
asked Aug 26, 2022 in * TF "Emb. Sys. and Rob." by ln (1k points)
0 votes
1 answer
ITE algorithm - clarification
asked Aug 22, 2022 in * TF "Emb. Sys. and Rob." by ln (1k points)
0 votes
1 answer
existential and universal successors
asked Aug 12, 2023 in * TF "Emb. Sys. and Rob." by zain (440 points)
 | Snow Theme by Q2A Market
Powered by Question2Answer
Imprint | Privacy Policy
...