Adding assumptions

By default the Solver believes only what the model writes down, read under the SysML v2 specification. That reading is often more permissive than what you have in your head: where you see “obviously there are exactly four wheels and they all weigh the same”, the specification may allow a fifth, unnamed wheel, or a wheel that overrides the default mass. The Solver then reports outcomes you never intended – correctly, because the model as written allows them.

Semantic overrides close these gaps. Each override is a named assumption you add on the command line; the Solver then analyzes the model as if the assumption were written into it. The output echoes every active override, so a result can always be traced to the assumptions it was computed under.

An example: default values

Create fleet.sysml. Every truck has a capacity that defaults to 10, and one named truck is declared without saying anything more about its capacity:

package Fleet {
    private import ScalarValues::Integer;
    part def Truck {
        attribute capacity : Integer default 10;
    }
    part fleet [1] {
        part trucks : Truck [2];
        part heavyTruck : Truck [1] subsets trucks;
    }
    assert constraint allStandard {
        Fleet::fleet::heavyTruck::capacity == 10
    }
}

Does heavyTruck have capacity 10? Intuitively yes – it never overrides the default. But in SysML v2 a default is exactly that: a value the usage is allowed to replace. The model does not say heavyTruck keeps it:

syside solver check -i fleet.sysml

{
  "assertions": [
    {
      "name": "Fleet::allStandard",
      "status": "violated",
      "counterexample": {
        "values": [
          ["Fleet::fleet::heavyTruck::capacity", "2"]
        ]
      }
    }
  ]
}

(Output truncated to the assertion list.)

Violated: nothing in the model prevents a capacity of 2. If your intent is “whatever does not override the default takes it”, say so with the sealed-defaults override:

syside solver check -i fleet.sysml --alt-semantics sealed-defaults

{
  "assertions": [
    { "name": "Fleet::allStandard", "status": "satisfied",
      "counterexample": null }
  ]
}

The full output also gains an alt_semantics section recording that sealed-defaults was active and what it means.

The shortcut: --alt-semantics free

Most users who reach for overrides want the same thing: “read my model literally – nothing exists beyond what I wrote.” No unnamed extra parts, no values silently overriding defaults, no messages arriving from outside the model. The free shorthand switches on the whole bundle of closed-world overrides at once:

syside solver check -i fleet.sysml --alt-semantics free

If the default reading keeps surprising you, try free first, and reach for individual overrides only when you need finer control.

Choosing individual overrides

Overrides are passed as a comma-separated list:

syside solver check -i model.sysml \
    --alt-semantics sealed-defaults,min-multiplicity

Each row below starts from the expectation you likely have; the override makes the Solver share it. Overrides marked ✓ are part of free.

If you expect that…	Use	free
Differently named parts are different things – heavyTruck and lightTruck cannot secretly be the same individual	distinct-subsetters	✓
A collection [2..*] has exactly the members you wrote, not extra unnamed ones; an optional [0..1] value you never set is absent	min-multiplicity	✓
Whatever does not override a default takes it	sealed-defaults	✓
A value you assign stays until the next assignment, with no unobserved changes in between	sticky-writes	✓
A state machine does not sit still while a transition is ready to fire	immediate-transitions	✓
The only messages are the ones your model sends – none arrive from outside	closed-messages	✓
A sent message is delivered without an unwritten delay	immediate-messages	✓
Messages route only through the interfaces you drew	closed-interfaces	✓
A state machine you wrote actually runs (rather than possibly never starting)	machines-run	✓
A claim about a definition means “check it at each of the written usages of that definition”	written-usages	✓
An expression mixing values that change over time reads them all at the same instant	simultaneous-expressions	✓
A package-level part rover means exactly one rover (saves you writing [1] everywhere)	singular-usages
An interface you drew exists in every scenario	interfaces-exist
Comparing values of different kinds (1 == "a", or anything with null) is simply false, not an error	mixed-equality-false
== between two sequences compares them element by element	sequence-equality
500 [milli * s] means 500 milliseconds	prefix-scaling

The last five are not in free because they go beyond closing the world: they either assert a fact the model does not write (singular-usages, interfaces-exist) or assign a meaning to syntax the specification leaves undefined (the other three).

The authoritative list, including the precise default each override replaces, comes from the tool itself:

syside solver overrides

A word of caution

An override is an assumption, and a check passed under an assumption is only as good as the assumption. When a check matters – a safety budget, a compliance requirement – prefer strengthening the model (fix the value, close the multiplicity, bind the parts) over adding overrides, and keep the alt_semantics section of the output alongside any result you report.