Doctor use case Diagram

-

Comments

Post a Comment

Popular posts from this blog

Semantics of LTL

-
Logical Paradigms in Computing Practical patterns of specifications: • It is impossible to get to a state where started holds, but ready does not hold: G¬(started ∧¬ready) • For any state, if a request (of some resource) occurs, then it will eventually be acknowledged: G(requested → F acknowledged). • A certain process is enabled infinitely often on every computation path: GF enabled. • Whatever happens, a certain process will eventually be permanently deadlocked: FG deadlock. • If the process is enabled infinitely often, then it runs infinitely often. GF enabled → GF running. • An upwards travelling lift at the second floor does not change its direction when it has passengers wishing to go to the fifth floor: G(floor2 ∧ directionup ∧ ButtonPressed5 → (directionup U floor5)). Here, our atomic descriptions are boolean expressions built from system variables, e.g., floor2. Important equivalences between LTL formulas: Definition: We say that two LTL formulas φ and ψ are semantically equivalent,...
Read more

Semantics of LTL

-
A transition system M=(S,→,L) is a set of states S endowed with a transition relation → (a binary relation), such that every s ∈ S has some s’∈ S with s → s’, and a labeling function L: S →P(Atoms). Transition systems are also simply called models. a model has a collection of states S, a relation →,saying how the system can move from state to state, and, associated with each state s, one has the set of atomic propositions L(s)which are true at that particular state. L is that it is just an assignment of truth values to all the propositional atoms. A transition system has more than one state, so this assignment depends on which state s the system is in: L(s) contains all atoms which are true in state s. All the information about a (finite) transition system M always be figured by using directed graphs whose nodes (which we call states) contain all propositional atoms that are true in that state. For example, if our system has only three states s0, s1 and s2; if the only possible transit...
Read more