Modelling using propositions, syntax and standards

Question

One of the first programs I wrote when learning Java was a console application modelling the operation of an elevator. I'm trying to teach myself propositional logic and so I thought, why not use the same example?

So, suppose I have been given the task of modelling the main functions of an elevator system using propositions and predicates...

• Opening and closing doors (allowing entrance and exit at appropriate times)
• Storing and responding to floor requests from users
• Processing information from sensors (elevator load, floor position and speed sensors)
• Displaying status information on the displays (at each floor and in the cab)

My Google searches have returned very little in the way of useful insight into how this should be done or any standards that might exist. What would be the best way to do this?

Would something like this be appropriate?:

$$ F = requestedFloor, L = loadSensor(load), C = loadSensor(capacity) $$ $$ F ∧ L < C → move(F) ∧ display: print(currentFloor) $$ $$ floorSensor(currentFloor) < F → move(up)$$ $$ floorSensor(currentFloor) > F → move(down)$$

Which is simple enough, right? If there is a floor requested and load is less than capacity then move to that floor. Also, print the floor to the display.

If anyone has any suggestions or can provide some examples of how I might model this I'd love to hear them.

Answer 1

Generally you have:

• Some boolean variables that collectively represent the current state, say $s,t,u$.

• Some boolean variables that collectively represents the inputs, say $i,j,k$. For instance, you might have one variable per sensor (assuming each sensor returns a boolean value).

• Some boolean variables that collectively represents the inputs, say $o,p,q$. For instance, you might have one variable per actuator (assuming each actuator can be either on or off).

• Some boolean variables that collectively represent the next state. You could give them a different name (e.g., $x,y,z$), but often, to help us remember the relationship to the variables for the current state, we used primed versions of the variables for the current state. So, the next state might be represented by $s',t',u'$.

Now, we introduce a predicate $\Psi(s,t,u,i,j,k,o,p,q,s',t',u')$ to represent the transition relation. The idea is that if this is true, it means the following: if you're in state $s,t,u$ and you receive inputs $i,j,k$, then you output $o,p,q$ AND transition to the state $s',t',u'$. You can use boolean logic to express the predicate $\Psi(s,t,u,i,j,k,o,p,q,s',t',u')$ as a boolean formula, using AND, NOT, OR, implication, etc.

Then you also need to describe the initial state of the system. For instance, it might be $(s,t,u)=(T,F,T)$.

As you can see, the notation can get a bit much. Often we collect all the variables associated with the current state into a vector $s$ of variables, $s=(s_1,\dots,s_k)$ where the state is $k$ bits (it is represented by $k$ boolean variables), and collect all of the variables associated with the input into a vector $i$ of variables, $i=(i_1,\dots,i_m)$; you similarly collect all the output variables into a vector $o=(o_1,\dots)$; and the next state is given by a vector $s'=(s'_1,\dots,s'_k)$ represents the next state.

As a generalization, you can consider variables that have more than two possible values (they aren't restricted to be booleans). Booleans are convenient for digital logic implementation, but more general variables can enable a specification that is easier to think about and understand.

So, basically, yes, this is compatible with the kind of approach you were showing.