The user can log out using a negative fact. To expose this capability to the user interface, we need to add a command to the view model.
The MachineViewModel is the right class for the command. It already has the LogOn command, and it is the DataContext of the correct view. We can start with a failing unit test. Add this to MachineViewModelTest.
public void UserLogsOff()
_viewModel.UserName = "alan1";
MachineViewModel starts from the Machine. The Machine partial class already has a LogOnUser() method. It should also have a LogOffUser() method. Call this from the command.
public ICommand LogOff
.Do(() => _machine.LogOffUser());
Now lets define this method. It needs to create a LogOff fact. The LogOff fact acts on the LogOn. So how do we get from Machine to the LogOn that needs to be negated? We already have a query for that: LogOns.
public void LogOffUser()
foreach (LogOn logOn in LogOns)
It may surprise you that we log off a user in a loop. Shouldn't there be only one user logged on to the machine? Yes, there should, but there is no way to prove that.
A query cannot be expected to return just one result. That's why the Factual modeling language requires an asterisk in the type of every query. It's reminding us that we cannot guarantee that only one fact will be returned. So even though our UI prevents
a second log on to the same machine, there is no way for Correspondence to know that we have taken those precautions. It is going to return a collection.
If the collection is empty, no one is logged on, and the LogOffUser method has no effect. If the collection contains one element, then one person is logged on, and the method logs them off. We have the desired effect in the expected cases, and we are still
safe for unexpected cases.
Run the unit test and you will see that it now passes. After logging off the user, the LogOns collection is empty.
Something else might surprise you if you think about it. When we add the LogOff fact, the LogOns collection changed. But yet we added that fact inside of a loop. Changing a collection while looping over it is supposed to throw an exception.
Correspondence changes the LogOns collection in a way that makes this pattern safe. The loop acts upon a snapshot of the collection taken upon entry. The change is only visible after someone else (like the unit test) takes another snapshot.
Lesson 3c: Enable and disable the negative command