(Gotzhein 19.7.98)

General remarks
---------------

Are the "functional needs" still "functional needs" with the time values
being introduced?

Emphasize: requirements are formalized as far as possible. The resulting
document will contain both formal and nonformal requirements. This is
typical for realistic development processes.

What means "roomOccupied"? "roomOccupied iff NOT roomEmpty", i.e.
"roomOccupied iff roomUsed, with T1=T2=T3=0"? 
Yes: a light scene can only be chosen with the room being occupied
No:  it is possible that a light scene is chosen with the room not
     being occupied

What means " *a* light scene is chosen"? When does it hold,
when does it become false? --> refinement
State --> "exists l. lightSceneChosen(l)"?

ad U1,U2.
---------
- How do T_U1 and T_U2 compare? T_U1 = T_U2? T_U1 > T_U2?

ad U3.
------
- How does T_U3b compare to T_U2? T_U3b = T_U2? Avoid too many different 
  time settings?
- Last chosen light scene: is "exists l. lightSceneChosen(l)" false already?

ad U4.
------
- How does T_U4b compare to T_U3b? T_U4b = T_U3b? Avoid too many different 
  time settings?

ad U5.
------
- Does pushing switches correspond to light scenes, i.e., are the predicates
  "lightSceneChosen(l)" affected?
- How does T_U5i compare to T_U5ii? T_U5i = T_U5ii? Avoid too many different 
  time settings?
- Are the times T_U5i and T_U5ii sufficiently small, so that the switch can
  not be pushed again before the light goes on/off? If no, what happens?

ad U6.
------
- In my understanding, PD-Sec.3.1.1/U6 says s.th. about "defining the light
  scenes" using the control panel, not selecting one
- if not: why not "light scene is chosen"? why a relationship between "light scene
  selected" and "light scene applied"? PD-Sec.3.1.1/U6 only refers to
  "light scene determined". Does it suffice here to say s.th. about the
  predicate "lightSceneChosen(l)"?

ad U7.
------
- see "ad U6".

ad U11.
-------
- what does "user is informed" mean? State?

ad U12.
-------
- ??? PD-Sec.3.1.1/U12 only states responsibilities in terms of some system
  architecture. What does "maintained" mean? 

ad U14.
-------
- ??? PD-Sec.3.1.1/U14 only states responsibilities in terms of some system
  architecture, and defines value domains, no behavior

ad U16.
-------
- see "ad U14"

ad U17.
-------
- How does T_U17 compare to T_U2? Avoid too many different time settings?

ad U18.
-------
- what means "if necessary" in PD-Sec.3.1.1/U18? Is this already made precise
  in U18?
- enter from another one: unclear in U18

ad U19.
-------
- How does T_U19 compare to T_U5i and T_U5ii? Avoid too many different 
  time settings?
- Is the time T_U19 sufficiently small, so that the switch can
  not be pushed again before the light goes on/off? If no, what happens?

ad FM1.
-------
- Difficult to formalize: calculate how much additional artificial light
  is needed to achieve the chosen light scene. Not only a matter of 
  light on or off!?

ad FM2.
-------
- "occupied"? see U18! is this part of the definition of "occupied", or
  would this be solved by preferences?

ad FM3.
-------

ad FM6.
-------
- "has turned" --> "turns"?
- "at least as long as ... has turned the light off and the ... is not
  occupied" --> "at least as long as the precondition is true"?

ad FM7.
-------
- what does "manager is informed" mean? State?
- can this be formalized?

ad NF1.
-------
- PD-Sec.3.2.1/NF1 is not a fail safe assumption! Fail safe would be that
  there is no outdoor light. This can always be overruled manually.

ad NF2.
-------
- conditionally defines the standard light scene. What is the standard light 
  scene in all other cases?
- "at least as ..." --> "at least as long as the precondition is true"?

ad NF3.
-------
- "at least as ..." --> "at least as long as the precondition is true"?

ad NF4.
-------
- question: motion detector --> motion detection? it may not be a single
  device, but a set of devices together with a controller
- use time? compare to NF1a, NF1b
- a) Whenever the motion detector works correctly for at least T_NF4a
     time units, then eventually within this time span, the motion
     detector value used by the system is equal to the motion detector
     value returned by the sensor with a maximum delay of T_2MD.
  b) Whenever the motion detector does not work correctly for at least
     T_NF4b time units, then eventually within this time span, the motion
     detector value used by the system is 'occupied' with a maximum delay
     of T_2MD and remains so at least as long as the precondition is true.

ad NF5.
-------
- "at least as ..." --> "at least as long as the precondition is true"?