Package: inet.linklayer.configurator.gatescheduling.z3

Z3GateScheduleConfigurator

simple module

This module provides a gate scheduling algorithm that uses the open source z3 SAT solver from Microsoft. In order to be able to use this module, the corresponding 'Z3 Gate Scheduling Configurator' feature must be enabled and the libz3-dev package must be installed.

This configurator computes the gate schedule by creating SAT variables for the transmission start/end times and reception start/end times for each packet for each flow in all network interfaces along the path. All communication network specific constraints such as transmission duration, propagation time, subsequent transmissions along the flow, queueing to avoid reordering packets, and taking traffic class priority into consideration are translated into SAT constraints among the above variables. All additional user constraints such as the maximum end-to-end delay and maximum jitter are also added to the model.

Finally, the SAT solver is used to find a solution that fulfills all constraints, and the result values are extracted and configured in the network.

The optimizeSchedule parameter can be used to control whether any solution is accepted or it should also be optimal with respect to the total end-to-end delay among all packets of all flows in the network.

Inheritance diagram

The following diagram shows inheritance relationships for this type. Unresolved types are missing from the diagram.

Extends

Name	Type	Description
GateScheduleConfiguratorBase	simple module	This module serves as a basis for gate scheduling configurator modules. It provides methods for derived modules to easily extract the input parameters from the network topology and also to carry out the actual configuration of the resulting schedule. The schedule is automatically configured in all of the PeriodicGate submodules of all queue submodules in the network interface MAC layer submodules. Besides, the application start offsets are also configured. This allows the derived modules to focus on the implementation of the actual scheduling algorithm.

Parameters

Name	Type	Default value	Description
gateCycleDuration	double		the globally used gate scheduling period in each PeriodicGate modules
configuration	object	[]	array of objects, see GateScheduleConfiguratorBase module documentation for more details example: [{name: "s1", type: "unicast", application: "app[0]", pcp: 0, gateIndex: 0, source: "wheel*", destination: "hud", packetLength: 100B, packetInterval: 5ms, maxLatency: 100us, maxJitter: 10us, pathFragments: [["a", "b", "c"]]}]
labelAsserts	bool	false
optimizeSchedule	bool	true

Properties

Name	Value	Description
display	i=block/cogwheel
class	Z3GateScheduleConfigurator

Direct method calls (observed)

call to	function	info
LayeredEthernetInterface	inet::NetworkInterface::receiveSignal	POST_MODEL_CHANGE
InterfaceTable	inet::InterfaceTable::findInterfaceByNodeInputGateId	findInterfaceByNodeInputGateId
InterfaceTable	inet::InterfaceTable::findInterfaceByNodeOutputGateId	findInterfaceByNodeOutputGateId

Source code

//
// This module provides a gate scheduling algorithm that uses the open source
// z3 SAT solver from Microsoft. In order to be able to use this module, the
// corresponding 'Z3 Gate Scheduling Configurator' feature must be enabled and
// the libz3-dev package must be installed.
//
// This configurator computes the gate schedule by creating SAT variables for
// the transmission start/end times and reception start/end times for each packet
// for each flow in all network interfaces along the path. All communication
// network specific constraints such as transmission duration, propagation time,
// subsequent transmissions along the flow, queueing to avoid reordering packets,
// and taking traffic class priority into consideration are translated into SAT
// constraints among the above variables. All additional user constraints such
// as the maximum end-to-end delay and maximum jitter are also added to the model.
//
// Finally, the SAT solver is used to find a solution that fulfills all constraints,
// and the result values are extracted and configured in the network.
//
// The optimizeSchedule parameter can be used to control whether any solution is
// accepted or it should also be optimal with respect to the total end-to-end delay
// among all packets of all flows in the network.
//
simple Z3GateScheduleConfigurator extends GateScheduleConfiguratorBase like IGateScheduleConfigurator
{
    parameters:
        bool labelAsserts = default(false);
        bool optimizeSchedule = default(true);
        @class(Z3GateScheduleConfigurator);
}

File: src/inet/linklayer/configurator/gatescheduling/z3/Z3GateScheduleConfigurator.ned