Skip to content

Statistical tests running the TSN showcase are dependent on Z3 version #1072

@torokati44

Description

@torokati44

The statistical tests on CI are currently running on Ubuntu 24.04, with an ancient Z3 version (v4.8.12).
My machine happens to have Z3 4.15.4. This finds a different solution for the gate schedules in these simulations, causing 1201 packets to be transmitted instead of 1200, and other differences as well:

showcases/tsn/combiningfeatures/gsandcs -c SAT for 0.2s FAIL (unexpected) (experiment = SAT, measurement = , replication = #0, module = TsnDumbbellNetwork.client1.app[1].io, name = packetSent:vector(packetBytes):starttime, value_stored = 0.0, value_current = 0.000043, relative_error = inf) in 14.254
showcases/tsn/gatescheduling/sat -c SAT for 0.2s FAIL (unexpected) (experiment = SAT, measurement = , replication = #0, module = TsnDumbbellNetwork.client1.app[1].io, name = packetSent:vector(packetBytes):starttime, value_stored = 0.0, value_current = 0.000046, relative_error = inf) in 10.047

This has caused issues multiple times already:
inet-framework/statistics@2e09b05
inet-framework/statistics@cfb0e52

Worked around by downloading and building INET with this very old Z3 version before updating the expected results.

Metadata

Metadata

Assignees

Labels

No labels
No labels

Type

No type

Projects

No projects

Milestone

No milestone

Relationships

None yet

Development

No branches or pull requests

Issue actions