Transaction controller model based tests

[kuujo]

This PR adds unit tests to the transaction controller using state transitions output by the TLC model. In total, it adds nearly 100k unit tests covering a wide array of scenarios to the transaction controller tests.

The way it works is it uses the TLA+ spec to generate test cases for every possible scenario that could occur within the onos-config stores. Based on the spec, the TLC model checker computes every possible state and transition and writes them to a file in JSON format, and the test then reads through those states and creates a new subtest for each state/transition. To run the test, the test runner sets up the transaction reconciler using mock stores that return the initial state of the system at the start of the test. For example, transaction.Store's Get method will be mocked to return the Transaction being reconciled, which the reconciler will retrieve at the start of the Reconcile call. Then, the test runner explores each possible transition from that state, and uses those transitions to create expected mock API calls. For example, if the controller is supposed to update the Configuration's committed values, it will mock an expected call to the configuration.Store's Update method, and when that method is called, the test runner will check the updates state to verify it's consistent with the TLA+ spec/model.

The tests also check states where the controller should not change anything (e.g. the change is waiting to be applied but the node is not connected to the target), and it tests scenarios where a failure can occur during the reconciliation call, resulting in a partial state change. For example, the TLA+ spec models scenarios where the reconciler updates the Configuration successfully but fails while updating the Transaction store state, e.g. due to a node or store failure. In this scenario, the test runner will configure the Configuration store to expect an update and the Transaction store to return an error indicating the failure.

Because the test cases are generated from the TLA+ spec, and because the TLA+ spec is checked for correctness, controller code that behaves consistent with the spec can be assumed to be correct, as well. In this case, the type of "correctness" the model checker has evaluated in the spec is:

• Transactions are guaranteed to be processed in serial order
• Configuration on the target is guaranteed to progress in order
• Changes are guaranteed to eventually be committed to the configuration and applied to the target
• Rollbacks are guaranteed to eventually be reverted in the configuration and on the target
• If a target rejects a change, no later change will be pushed to the target until the failed change has been rolled back
• No deadlocks are possible within the controllers
• All this while nodes disconnect, crash and restart; targets crash and restart; before during and after every possible operation
• etc

In short, the algorithm guarantees order and progress and is devoid of deadlock paths, regardless of when or how the node, network, or target may fail.

[SeanCondon]

hard to argue with a well formatted tar.gz ;-)

[SeanCondon]

hi @kuujo - can we try to get this merged?

[gab-arrobo]

retest this please

[gab-arrobo]

@SeanCondon can this PR be merged? You already approved it. What is missing?

[SeanCondon]

@kuujo - Are we still good to merge this?
@gab-arrobo - let's wait for Jordan's approval