Assert that a spec passes model checking with the given configuration.

The config is passed to ExTLA.ModelChecker.run/2, whose options it takes. One of them matters here more than anywhere: liveness is off by default. run/2 defaults check_liveness: to false, and so does this, so a temporal property mix extla.check checks is not checked by assert_spec/2 unless the config says check_liveness: true.

Options, beyond ExTLA.ModelChecker.config/0

• allow_incomplete: true — pass even if the state limit was reached or a state constraint bounded the run. Default false.
• strict_coverage: true — fail on a never-enabled action or a vacuous property. Default false: they are reported, not fatal.