test(mbt): MBT for round state machine

[hvanz]

Closes #45

[hvanz]

@josef-widder Please check if this makes sense, together with the new conditions in NewRoundProposerCInput and NewRoundCInput.

[romac]

@josef-widder I am wondering if we can remove the NoStep step and merge it with NewRoundStep? (now called UnstartedStep)

[josef-widder]

NoStep actually is used to record that the last consensus action did not change the step variable. See

    pure def recordStepChange(old: DriverState, new: DriverState) : DriverState =
        if (old.cs.step == new.cs.step)
            { ...new, pendingStepChange: NoStep }
        else
            { ...new, pendingStepChange: new.cs.step}

So we shouldn't merge it. But perhaps it eventually makes sense to rename it to NoStepChange.

But perhaps inside the consensus state, it makes sense to initialize to NewRoundStep. I just realized that the step variable seems not to be initialized properly in the arXiv paper, so we should think about it before we change anything.

[josef-widder]

@josef-widder Please check if this makes sense, together with the new conditions in NewRoundProposerCInput and NewRoundCInput.

It think it is OK, as there is also a new condition in RoundSkipCInput(r)

[romac]

I tried removing NoStep and using a sum type for pendingStepChange:

type StepChange =
  | NoStepChange
  | SomeStepChange(Step)

// ...

pendingStepChange: StepChange

// ...

pure def recordStepChange(old: DriverState, new: DriverState) : DriverState =
    if (old.cs.step == new.cs.step)
        { ...new, pendingStepChange: NoStepChange }
    else
        { ...new, pendingStepChange: SomeStepChange(new.cs.step) }

which works fine but then I could not get the MBT tests to work properly, and I don't want to mess too much with them right now.

So let's leave it like that for now.

[romac]

Here the issue is that the spec does two steps at once here, whereas the round state machine needs whoever is driving it to feed it back a value to propose.

I am a bit surprised that the whole test even goes through given that we never do so in the test runner, need to dig in further.

@hvanz Do you have an idea for why that is?

[hvanz]

I'm not sure why. I think it's related to my comment above about the proposal value not used https://github.com/informalsystems/malachite/pull/120/files#r1428373893