spec: Improve readability and quality of quint spec

[martin-hutle]

The quint specification is sometimes inconsistent in naming and lacks documentation of the sometimes complex structure between the driver calls.
In particular the naming is inconsistent for

• Votekeeper, vk, Bookkeeper bk
• driverstate ds vs es
• ns and state for NodeStates
• val, p, address for consensus participants
• DriverOutput vs toDriverResult

There is a name clash between

• validators (val) as in valset and values
• proposals and proposers
  Readability would profit from a consistent way to distinguish them .

Other issues are / improvements would be

• replace consistently .with("") with (...x, )
• split functionality for NodeState and DriverState in different files
• ConsensusCall is never used
• check if nextActionCommand is really needed. Maintaining two functions with same functionality can lead to inconsistencies
• The handling of PendingDInput is a bit obscure:
  • in nextAction an input is chosen from pendingInputs and PendingDInput returned
  • driverLogic discards the selected input
  • handlePendingInput selects again from pendingInputs (and removes this then)
• Consensus errors (ErrorOutput) are never used, tested or recorded
• Adding helpful comments and function descriptions to the files (in particular for driver.qnt)

[cason]

Can be seen as part of #468.