Model-based testing seems to ignore command preconditions when model implementation is mutable?

[nyctef]

First off: thanks for fscheck! It's been a great library so far :)

Not exactly sure what's going on here, but I've managed to narrow it down to the following reproduction based on the C# Counter example in the docs:

summary of changes

• Counter becomes PositiveCounter (throws if you attempt to decrement below zero)
• Dec command class now has a precondition to avoid trying to decrement below zero in the test
• the plain int model becomes a mutable class IntModel (this is to represent my actual use case where I needed to use a List<T> as the model)
  this part in particular appears to be required to reproduce the issue

expected behavior: the test should pass (because I've not included the original bug in Counter from the docs)

actual behavior: the spec attempts to decrement before incrementing:

System.Exception : Falsifiable, after 4 tests (0 shrinks) (StdGen (161469180, 297185542)):
Original:
[dec; dec]
with exception:
System.Exception: Can't decrement below zero!
  [ stack trace follows... ]

public class PositiveCounter
{
    private int _value = 0;

    public void Inc()
    {
        _value += 1;
    }

    public void Dec()
    {
        if (_value == 0)
        {
            throw new Exception("Can't decrement below zero!");
        }

        _value -= 1;
    }

    public int Get()
    {
        return _value;
    }
}

public class IntModel
{
    public int Value { get; set; } = 0;
}

public class CounterSpec : ICommandGenerator<PositiveCounter, IntModel>
{
    public Gen<Command<PositiveCounter, IntModel>> Next(IntModel value)
    {
        return Gen.Elements(
            new Command<PositiveCounter, IntModel>[]
            {
                new Inc(),
                new Dec()
            });
    }

    public PositiveCounter InitialActual => new PositiveCounter();

    public IntModel InitialModel => new();

    private class Inc : Command<PositiveCounter, IntModel>
    {
        public override PositiveCounter RunActual(PositiveCounter c)
        {
            c.Inc();
            return c;
        }

        public override IntModel RunModel(IntModel m)
        {
            m.Value += 1;
            return m;
        }

        public override Property Post(PositiveCounter c, IntModel m)
        {
            return (m.Value == c.Get()).ToProperty();
        }

        public override string ToString() => "inc";
    }

    private class Dec : Command<PositiveCounter, IntModel>
    {
        public override bool Pre(IntModel model) => model.Value > 0;

        public override PositiveCounter RunActual(PositiveCounter c)
        {
            c.Dec();
            return c;
        }

        public override IntModel RunModel(IntModel m)
        {
            m.Value -= 1;
            return m;
        }

        public override Property Post(PositiveCounter c, IntModel m)
        {
            return (m.Value == c.Get()).ToProperty();
        }

        public override string ToString() => "dec";
    }
}


class Tests
{
    [Test]
    public void CounterTest()
    {
        var config = Configuration.QuickThrowOnFailure;
        // config.MaxNbOfTest = 10_000;
        config.Replay = Random.StdGen.NewStdGen(161469180, 297185542);
        new CounterSpec().ToProperty().Check(config);
    }
}

[kurtschelfthout]

Yes it's not advisable to use mutable types as the model, this will confuse the thing endlessly. Try using ImmutableList instead, or cloning the model before returning it.

[nyctef]

Makes sense I guess, but it's kind of strange that the implementation class in a spec can be mutable while the model class must be immutable. Maybe this can be made explicit in the docs?