## Ex3.3: transition relation semantics (HRU model)

felicis
BASIC-Programmierer
Beiträge: 114
Registriert: 14. Apr 2015 20:25

### Ex3.3: transition relation semantics (HRU model)

Hi,

I would like to use the constraint for conditional requests (slide 21) for exercise part a). It would help me very much if the "implies" would be a "is equivalent to". Is this valid, or do I allow wrong semantics for the requests if I make this change?

best
felicis

Markus Tasch
BASIC-Programmierer
Beiträge: 124
Registriert: 11. Sep 2015 10:57

### Re: Ex3.3: transition relation semantics (HRU model)

As usual with formal semantics, they have to be used as they are defined. Therefore, stick to "implies" instead of "if and only if". Potentially your problem in solving Exercise 3.3a) is solved by taking another look at the definition on Slide 25 (Module 04).
Markus Tasch, M.Sc.
Modeling and Analysis of Information Systems
Department of Computer Science, TU Darmstadt

felicis
BASIC-Programmierer
Beiträge: 114
Registriert: 14. Apr 2015 20:25

### Re: Ex3.3: transition relation semantics (HRU model)

Doesn't the Definition on slide 4.25 imply the equivalence?
If the transition relation is the greatest set of (single) transitions, which comply with all constraints, there cannot be any single transition which complies with the constraints, but is not present in the transition relation, can't there?
Can I just add this to my proofs? Otherwise I would have to completely rebuild my proof structure.....

best
felicis

EDIT: typo

Markus Tasch
BASIC-Programmierer
Beiträge: 124
Registriert: 11. Sep 2015 10:57

### Re: Ex3.3: transition relation semantics (HRU model)

Doesn't the Definition on slide 4.25 imply the equivalence?
Yes, you can prove the equivalence based on definition on slide 4.25. Nevertheless, you would have to prove a corrsponding theorem to use this result in a formal proof in a clean fashion.

For Exercise 3.3:
Here a convincing argument using the formal definitions is enough because Exercise 3.3 does not ask for a formal proof.
Markus Tasch, M.Sc.
Modeling and Analysis of Information Systems
Department of Computer Science, TU Darmstadt