acassimiro/tsnsched

Automated Schedule Generation for Time-Sensitive Networks (TSN).

tsnsched's Issues

How to write code for one device sending two or more TSN flows?

Thanks for your code, Cassimiro.
In the example code, when need a tsn terminal, you define it like this:
"Device dev0 = new Device(1000, 0, 1000, 1625);"

Does it mean that one device can only send one tsn flow? How can it be allowed if we want the device to send two more TSN flows at one port?

Improve code quality

Improve the code quality by utilizing static analysis tools such as SonarLint (Eclipse plugin)

Make logging and console outputing optional

Make them parameters of the command line.

Enable control of the output file name

Currently our outputs have default names. Enable custom naming.

Simplify language of README

The documentation is currently very extensive but also hard to read. I propose the following tools to improve it:

• Hemingway Editor

Hemingway makes your writing bold and clear. It's like a spellchecker, but for style. It makes sure that your reader will focus on your message, not your prose.

• LanguageTool or Grammarly

LanguageTool is an Open Source proofreading software for English, French, German, Polish, Russian, and more than 20 other languages. It finds many errors that a simple spell checker cannot detect.

Compose clear, mistake-free writing that makes the right impression with Grammarly’s writing assistant.

Two flows with different cycle merge into the same link

Hi,
Thanks for your code. I am running an example on the project.
My example has two flows as follows:

Flow flow0 = new Flow(Flow.UNICAST);
flow0.setStartDevice(dev4);
flow0.addToPath(switch0);
flow0.addToPath(switch2);
flow0.setEndDevice(dev10);
flow0.setFlowSendingPeriodicity(2000);


Flow flow1 = new Flow(Flow.UNICAST);
flow1.setStartDevice(dev5);
flow1.addToPath(switch1);
flow1.addToPath(switch2);
flow1.setEndDevice(dev10);
flow1.setFlowSendingPeriodicity(3000);

The topology is:

Dev4 -> SW0 -> SW2 -> Dev10
                ^
                |
Dev5 -> Sw1 -> 

And the result is:

>>>> INFORMATION OF SWITCH: switch0 <<<<
    Port list - 
        => Port name:       switch0Port1
        Connects to:     switch2
        Cycle start:    0.0
        Cycle duration: 2000.0
        Fragments:       flow1Fragment1, 
        Priority number: 7
          Index 0 Slot start:      1949.088
          Index 0 Slot duration:   8.004
        ------------------------


>>>> INFORMATION OF SWITCH: switch1 <<<<
    Port list - 
        => Port name:       switch1Port1
        Connects to:     switch2
        Cycle start:    0.0
        Cycle duration: 3000.0
        Fragments:       flow2Fragment1, 
        Priority number: 7
          Index 0 Slot start:      2940.996
          Index 0 Slot duration:   8.0
        ------------------------


>>>> INFORMATION OF SWITCH: switch2 <<<<
    Port list - 
        => Port name:       switch2Port9
        Connects to:     dev10
        Cycle start:    0.0
        Cycle duration: 1000.0
        Fragments:       flow1Fragment2, flow2Fragment2, 
        Priority number: 7
          Index 0 Slot start:      949.992
          Index 0 Slot duration:   50.0
        ------------------------

I notice that Cycle duration of Switch2 is 1ms. It means that there is a slot in 1ms. But cycle of flow0 is 2ms, and cycle of flow1 is 3ms. There will has two slot without packets within every 6ms.

I think it is better that the Cycle duration of Switch2 shall be 6ms (i.e. Least Common Multiple of two flow). In each cycle, there are four time slots .

Which part of the code do I need to modify？
Thanks

Failed to run the example

Hello, I am using Ubuntu18.04, JAVA-8, Z3 4.8.10 or Z34.9.1 I have also used, but when I run the example, there is always an error, the error is as shown below, do you have a better suggestion

when set two flows with different periods,cant get the reult,which log the "The specified constraints MIGHT NOT be satisfiable"

here is the test code,which overwrites the SmallScenario.java
the network is 4 devices and 6 switches and 2 flows,when flow1 send at 2ms, flow2 send at 2ms，the result is ok
when flow1 send at 2ms, flow2 send at 3ms，the result is NOT be satisfiable.
but i dont know why,becasue the z3 just give the final result,but which constraint is unknown.

package com.tsnsched.generated_scenarios;
import java.util.;
import java.io.;
import com.tsnsched.core.nodes.;
import com.tsnsched.core.components.Cycle;
import com.tsnsched.core.components.Flow;
import com.tsnsched.core.components.PathNode;
import com.tsnsched.core.network.;
import com.tsnsched.core.schedule_generator.*;
import com.tsnsched.core.components.Port;

public class SmallScenario {
public void runTestCase(){

	/*
	 * GENERATING DEVICES
	 */
	Device ccu = new Device(1000, 0, 1000, 1500);
	ccu.setName("ccu");
	
	Device ccu2 = new Device(1000, 0, 1000, 1500);
	ccu2.setName("ccu2");
	
	Device tcu = new Device(1000, 0, 1000, 1500);
	tcu.setName("tcu");
	
	Device bcu = new Device(1000, 0, 1000, 1500);
	bcu.setName("bcu");

	/*
	 * GENERATING SWITCHES
	 */
	TSNSwitch switch0 = new TSNSwitch("switch0", 100, 1, 125, 1, 400, 3000);
	TSNSwitch switch1 = new TSNSwitch("switch1", 100, 1, 125, 1, 400, 3000);
	TSNSwitch switch2 = new TSNSwitch("switch2", 100, 1, 125, 1, 400, 3000);
	TSNSwitch switch3 = new TSNSwitch("switch3", 100, 1, 125, 1, 400, 3000);
	TSNSwitch switch4 = new TSNSwitch("switch4", 100, 1, 125, 1, 400, 3000);
	TSNSwitch switch5 = new TSNSwitch("switch5", 100, 1, 125, 1, 400, 3000);
	
	/*
	 * GENERATING SWITCH CONNECTION PORTS
	 */
	Cycle cycle0 = new Cycle(50);
	Port port0 = switch0.createPort(switch1, cycle0);//switch0 use x11 to connect switch1 
	port0.setPortNum(11);
	port0.setName(port0.getName()+ "Port"+ "11");
	
	Cycle cycle1 = new Cycle(50);
	Port port1 = switch1.createPort(switch0, cycle1);
	port1.setPortNum(4);
	port1.setName(port1.getName()+ "Port"+ "4");
	

	Cycle cycle2 = new Cycle(50);
	Port port2 = switch1.createPort(switch2, cycle2);	
	port2.setPortNum(1);
	port2.setName(port2.getName()+ "Port"+ "1");
	
	Cycle cycle3 = new Cycle(50);
	Port port3 = switch2.createPort(switch1, cycle3);
	port3.setPortNum(2);
	port3.setName(port3.getName()+ "Port"+ "2");
	
	Cycle cycle4 = new Cycle(50);
	Port port4 = switch2.createPort(switch3, cycle4);
	port4.setPortNum(1);
	port4.setName(port4.getName()+ "Port"+ "1");
	
	Cycle cycle5 = new Cycle(50);
	Port port5 = switch3.createPort(switch2, cycle5);
	port5.setPortNum(2);
	port5.setName(port5.getName()+ "Port"+ "2");
	
	Cycle cycle6 = new Cycle(50);
	Port port6 = switch3.createPort(switch4, cycle6);
	port6.setPortNum(1);
	port6.setName(port6.getName()+ "Port"+ "1");
	
	Cycle cycle7 = new Cycle(50);
	Port port7 = switch4.createPort(switch3, cycle7);
	port7.setPortNum(2);
	port7.setName(port7.getName()+ "Port"+ "2");
	
	Cycle cycle8 = new Cycle(50);
	Port port8 = switch4.createPort(switch5, cycle8);
	port8.setPortNum(4);
	port8.setName(port8.getName()+ "Port"+ "4");
	
	Cycle cycle9 = new Cycle(50);
	Port port9 = switch5.createPort(switch4, cycle9);	
	port9.setPortNum(11);
	port9.setName(port9.getName()+ "Port"+ "11");


	
	
	/*
	 * LINKING SWITCHES TO DEVICES
	 */
	Cycle cycle10 = new Cycle(50);
	Port port10 = switch0.createPort(ccu, cycle10);
	port10.setPortNum(9);
	port10.setName(port10.getName()+ "Port"+ "9");
	
	Cycle cycle11 = new Cycle(50);
	Port port11 = switch5.createPort(tcu, cycle11);
	port11.setPortNum(9);
	port11.setName(port11.getName()+ "Port"+ "9");
	
	Cycle cycle12 = new Cycle(50);
	Port port12 = switch2.createPort(ccu2, cycle12);
	port12.setPortNum(9);
	port12.setName(port12.getName()+ "Port"+ "9");
	
	
	Cycle cycle13 = new Cycle(50);
	Port port13 = switch4.createPort(bcu, cycle13);
	port13.setPortNum(9);
	port13.setName(port13.getName()+ "Port"+ "9");
	
	/*
	 * GENERATING FLOWS
	 */
	LinkedList<PathNode> nodeList;

	Flow flow1 = new Flow(1,0,2000);
	//Flow flow1 = new Flow(Flow.UNICAST);
	flow1.setStartDevice(ccu);
	flow1.addToPath(ccu,switch0);
	flow1.addToPath(switch0,switch1);
	flow1.addToPath(switch1,switch2);
	flow1.addToPath(switch2,ccu2);
	flow1.addToPath(switch2,switch3);
	flow1.addToPath(switch3,switch4);
	flow1.addToPath(switch4,bcu);
	flow1.addToPath(switch4,switch5);
	flow1.addToPath(switch5,tcu);
	
	flow1.setPriorityValue(5);
	flow1.setFixedPriority(true);
	//flow1.setPacketSize(1500);
	//flow1.setFlowMaximumLatency(1000);
	flow1.setFlowSendingPeriodicity(2000);
	
	
	Flow flow2 = new Flow(1,0,2000);
	//Flow flow2 = new Flow(Flow.UNICAST);
	flow2.setStartDevice(ccu);
	flow2.addToPath(ccu,switch0);
	flow2.addToPath(switch0,switch1);
	flow2.addToPath(switch1,switch2);
	flow2.addToPath(switch2,ccu2);
	flow2.addToPath(switch2,switch3);
	flow2.addToPath(switch3,switch4);
	flow2.addToPath(switch4,bcu);
	flow2.addToPath(switch4,switch5);
	flow2.addToPath(switch5,tcu);
	flow2.setPriorityValue(5);
	flow2.setFixedPriority(true);	
	//flow2.setPacketSize(1500);
	flow2.setFlowSendingPeriodicity(2000);//when set it to 3ms，the result is not satisfied
	//flow2.setFlowMaximumLatency(1000);
	
	/*
	 * GENERATING THE NETWORK
	 */
	Network net = new Network(25);
	net.addDevice(ccu);
	net.addDevice(ccu2);
	net.addDevice(tcu);
	net.addDevice(bcu);

	net.addSwitch(switch0);
	net.addSwitch(switch1);
	net.addSwitch(switch2);
	net.addSwitch(switch3);
	net.addSwitch(switch4);
	net.addSwitch(switch5);
	
	net.addFlow(flow1);
	net.addFlow(flow2);
	
	ScheduleGenerator scheduleGenerator = new ScheduleGenerator(false);
	scheduleGenerator.generateSchedule(net);


}

}

Add configuration options at port level.

Enable configuration for the following properties at port level:

• timeToTravel float (input)
• portSpeed float (input)
• gbSize float (input)
• name string

Enable user to control port name

There is a bug after modifying M1 chip

Hello, I installed all the dependencies according to the tutorial, but there are bugs similar to others.
Then I found that the bug occurred after the M1 compatibility was modified.
So other users can go back to the version before M1 modification, and then they can run normally.

i am chinese
您好，我按教程安装了所有的依赖，但是出现了跟其他人类似的bug。
然后我发现，应该是在修改M1兼容性以后，出现了bug。
所以其他用户可以回退到M1修改之前的那个版本，就可以正常运行了。

Allow the usage of priorityValue without fixedPriority

If the flow has a priorityValue, then the priority should be fixed. We should not need to specify it.

The flow type setting problem

I set flow type as UNICAST in my java file, but the output file (.log) show the flow is MULTICAST.
My java file screenshot:

The output file screenshot:

Documentation of new features

TSNsched now enables new features such as JSON and XML input support and more effective scheduling methodologies. This needs to be documented.

Java version issue when trying the example

Hi!

Apologies for the beginner question. I am trying to run the example use case under the Script directory. The ./install-dependencies.sh script finished without issues until the example. At first, I unfortunately had this error when running the example script with Java 8 or 11:

$ ./generateSchedule.sh example.java
rm: cannot remove 'output/*': No such file or directory
:./libs/com.microsoft.z3.jar:./libs/gson-2.8.6.jar:./libs/java-json.jar:./libs/TSNsched.jar
UseCase.java:1: error: cannot access JSONParser
import com.tsnsched.core.interface_manager.JSONParser;
                                          ^
  bad class file: ./libs/TSNsched.jar(/com/tsnsched/core/interface_manager/JSONParser.class)
    class file has wrong version 61.0, should be 55.0
    Please remove or make sure it appears in the correct subdirectory of the classpath.
[...]

It seemed like the .jar lib files were complied using Java 17 (version 61.0 shown above) while version 11 was expected (version 55.0). The same happens when trying with Java 8, except 55.0 is replaced by 52.0.

I then tried to install Java 17 and run the script with it, but I get a different error:

$ ./generateSchedule.sh example.java                                        
rm: cannot remove 'output/*': No such file or directory
:./libs/com.microsoft.z3.jar:./libs/gson-2.8.6.jar:./libs/java-json.jar:./libs/TSNsched.jar
Exception in thread "main" java.lang.NoSuchMethodError: 'void com.microsoft.z3.Solver.add(com.microsoft.z3.Expr[])'
        at com.tsnsched.core.components.Port.setUpCycle(Port.java:1377)
        at com.tsnsched.core.nodes.TSNSwitch.setUpCycleSize(TSNSwitch.java:418)
        at com.tsnsched.core.schedule_generator.ScheduleGenerator.configureNetwork(ScheduleGenerator.java:159)
        at com.tsnsched.core.schedule_generator.ScheduleGenerator.generateSchedule(ScheduleGenerator.java:257)
        at UseCase.runTestCase(UseCase.java:453)
        at GenerateScheduleJavaInput.main(GenerateScheduleJavaInput.java:15)
mv: cannot move 'output.txt' to 'output/example.java.out': No such file or directory
mv: cannot stat 'log.txt': No such file or directory
mv: cannot stat 'output.json': No such file or directory
Ending execution

Is there an obvious mistake? I see that the installation script installs Java 8, but I haven't figured out what could be wrong.
Thank you for your help!

Porting to C++ and merging into INET/OMNeT++

Hi!

My name is Levente Mészáros and I'm one of the core developers of the INET Framework for the OMNeT++ network simulator tool . Recently, INET has been extended with TSN features and I found your TSNsched project very interesting. I would like to port it to C++ and include it in the INET framework project. In the future, I'm planning to add stream redundancy support. Of course, I would give all credits to you in the source files. Do you mind this?

Best wishes,
levy

Use Google Java Code Style

Installing the coding style settings in Eclipse

Google Java Code Style

Download the eclipse-java-google-style.xml. Under Window/Preferences select Java/Code Style/Formatter. Import the settings file by selecting Import.

Configure save actions to automatically format your code when saving

In the Preferences menu, select Java -> Editor -> Save Actions.

Select Perform the selected actions on save.
Select Format source code.
Click the Formatter” link and ensure the “GoogleStyle formatter is selected as active.
Click OK.

Now, whenever you make changes to your code, you can use the format source code menu item, or just save the file and formatting will be applied automatically.

Incremental on-line scheduling

Hi,

I was wondering if it is possible to extend TSNsched to do incremental flow scheduling. If yes, how to do it?

generateSchedule.sh example.java

how can i solve this issue

about cycle start time

Hello,
I used this tool to run a simple test case, and I have a question: the result shows that the cycle start time of the switches are different, which brings inconvenience to the manual verification results later. Can we fix the cycle start time of all switches to be the same? For example, both are 0.

thank you!

INFORMATION OF SWITCH: switch0 <<<<
Port list -
=> Port name: switch0Port1
Connects to: switch2
Cycle start: 0.0
Cycle duration: 1000.0
Fragments: flow1Fragment1,
Slots per prt: 1
Priority number: 5
Index 0 Slot start: 0.5
Index 0 Slot duration: 52.5
------------------------

INFORMATION OF SWITCH: switch2 <<<<
Port list -
=> Port name: switch2Port2
Connects to: switch3
Cycle start: 1.0
Cycle duration: 1000.0
Fragments: flow1Fragment2, flow2Fragment2, flow3Fragment2,
Slots per prt: 1
Priority number: 5
Index 0 Slot start: 0.5
Index 0 Slot duration: 52.5
------------------------

INFORMATION OF SWITCH: switch3 <<<<
Port list -
=> Port name: switch3Port9
Connects to: dev15
Cycle start: 28.0
Cycle duration: 1000.0
Fragments: flow1Fragment3, flow2Fragment3, flow3Fragment3, flow4Fragment2,
Slots per prt: 1
Priority number: 5
Index 0 Slot start: 0.5
Index 0 Slot duration: 52.5
------------------------

INFORMATION OF SWITCH: switch4 <<<<
Port list -
=> Port name: switch4Port2
Connects to: switch2
Cycle start: 0.0
Cycle duration: 1000.0
Fragments: flow2Fragment1, flow3Fragment1,
Slots per prt: 1
Priority number: 5
Index 0 Slot start: 0.5
Index 0 Slot duration: 52.5
------------------------

INFORMATION OF SWITCH: switch5 <<<<
Port list -
=> Port name: switch5Port3
Connects to: switch3
Cycle start: 14.0
Cycle duration: 1000.0
Fragments: flow4Fragment1,
Slots per prt: 1
Priority number: 5
Index 0 Slot start: 0.5
Index 0 Slot duration: 52.5
------------------------

no output

Hi,

I have all dependencies installed successfully by running "sudo ./install-dependencies.sh".

But, after running the following commands,
cd ./Script
./generateSchedule.sh example.java

It display the following text:
:./libs/com.microsoft.z3.jar:./libs/gson-2.8.6.jar:./libs/java-json.jar:./libs/TSNsched.jar
mv: cannot stat 'log.txt': No such file or directory
Ending execution

and Script/output/example.java.out is empty.

Can you help me?

Build a better command line output interface

Add support for JSONs as output for TSNsched.

What went wrong?

Hello, thanks for your code, but I have some problems. I use version Ubuntu18.04, z3-4.8.13, but running examples always report this error。Please advise?

kaiguoguo@kaiguoguo-virtual-machine:~/Desktop/TSNsched/Script$ ./generateSchedule.sh example.java
:./libs/com.microsoft.z3.jar:./libs/gson-2.8.6.jar:./libs/java-json.jar:./libs/TSNsched.jar
Exception in thread "main" java.lang.NoSuchMethodError: 'void com.microsoft.z3.Solver.add(com.microsoft.z3.Expr[])'
at com.tsnsched.core.components.Port.setUpCycle(Port.java:1377)
at com.tsnsched.core.nodes.TSNSwitch.setUpCycleSize(TSNSwitch.java:418)
at com.tsnsched.core.schedule_generator.ScheduleGenerator.configureNetwork(ScheduleGenerator.java:159)
at com.tsnsched.core.schedule_generator.ScheduleGenerator.generateSchedule(ScheduleGenerator.java:257)
at UseCase.runTestCase(UseCase.java:453)
at GenerateScheduleJavaInput.main(GenerateScheduleJavaInput.java:15)
mv: cannot stat 'log.txt': No such file or directory
mv: cannot stat 'output.json': No such file or directory
Ending execution

Results are different between command line(generateSchedule.sh) and Eclipse java project(use src/*.java files)?

Hello,
i run tests from cmd and Eclipse java project. The test case is same(Script/example.java).But results are a little different between command line(generateSchedule.sh) and Eclipse java project(use src/.java files).
Is there something different from Scripts/libs/.jar and src/*java files?

Result.tar.gz

I also confused about the value "Fragment slot duration : 28.375(28.5)" , because packetsize is 1625, that means the packet need 13 microsecond to transmit. so i think fragment slot duration 14 microseconds is enough. How to get the value 28?

FLOW LIST:
Flow name: flow1
Start dev. first t1: 0
Start dev. HC: 1000
Start dev. packet periodicity: 1000
Flow type: Multicast
List of leaves: dev15, dev16, dev17, dev18, dev19,
Path to dev15: dev4, switch0(flow1Fragment1), switch4(flow1Fragment2), switch3(flow1Fragment3), dev15,
Path to dev16: dev4, switch0(flow1Fragment1), switch4(flow1Fragment2), switch3(flow1Fragment4), dev16,
Path to dev17: dev4, switch0(flow1Fragment1), switch4(flow1Fragment2), switch3(flow1Fragment5), dev17,
Path to dev18: dev4, switch0(flow1Fragment1), switch4(flow1Fragment2), switch3(flow1Fragment6), dev18,
Path to dev19: dev4, switch0(flow1Fragment1), switch4(flow1Fragment2), switch3(flow1Fragment7), dev19,

Fragment name: flow1Fragment1
    Fragment node: switch0
    Fragment next hop: switch4
    Fragment priority: 0
    Fragment slot start 0: 0.125
    Fragment slot duration 0 : 28.375
    Fragment times-
      (0) Fragment departure time: 0.0
      (0) Fragment arrival time: 1.0
      (0) Fragment scheduled time: 14.0
      ----------------------------
Fragment name: flow1Fragment2
    Fragment node: switch4
    Fragment next hop: switch3
    Fragment priority: 0
    Fragment slot start 0: 0.125
    Fragment slot duration 0 : 28.375
    Fragment times-
      (0) Fragment departure time: 14.0
      (0) Fragment arrival time: 15.0
      (0) Fragment scheduled time: 28.0
      ----------------------------
Fragment name: flow1Fragment3
    Fragment node: switch3
    Fragment next hop: dev15
    Fragment priority: 0
    Fragment slot start 0: 0.125
    Fragment slot duration 0 : 28.375
    Fragment times-
      (0) Fragment departure time: 28.0
      (0) Fragment arrival time: 29.0
      (0) Fragment scheduled time: 42.0
      ----------------------------
Fragment name: flow1Fragment4
    Fragment node: switch3
    Fragment next hop: dev16
    Fragment priority: 0
    Fragment slot start 0: 0.125
    Fragment slot duration 0 : 28.375
    Fragment times-
      (0) Fragment departure time: 28.0
      (0) Fragment arrival time: 29.0
      (0) Fragment scheduled time: 42.0
      ----------------------------
Fragment name: flow1Fragment5
    Fragment node: switch3
    Fragment next hop: dev17
    Fragment priority: 0
    Fragment slot start 0: 0.125
    Fragment slot duration 0 : 28.375
    Fragment times-
      (0) Fragment departure time: 28.0
      (0) Fragment arrival time: 29.0
      (0) Fragment scheduled time: 42.0
      ----------------------------
Fragment name: flow1Fragment6
    Fragment node: switch3
    Fragment next hop: dev18
    Fragment priority: 0
    Fragment slot start 0: 0.125
    Fragment slot duration 0 : 28.375
    Fragment times-
      (0) Fragment departure time: 28.0
      (0) Fragment arrival time: 29.0
      (0) Fragment scheduled time: 42.0
      ----------------------------
Fragment name: flow1Fragment7
    Fragment node: switch3
    Fragment next hop: dev19
    Fragment priority: 0
    Fragment slot start 0: 0.125
    Fragment slot duration 0 : 28.375
    Fragment times-
      (0) Fragment departure time: 28.0
      (0) Fragment arrival time: 29.0
      (0) Fragment scheduled time: 42.0
      ----------------------------

Support for multiple streams sourced at a single Device

Hello and thanks for making your source code public!

I am wondering if there is a way to specify multiple streams sourced at a single Talker Device and let solver consider this in the GCL computation? The Device class interface seems to take as input only a single set of packetPeriodicity + XConstraintTime + packetSize arguments.

Thanks!

Build a better command line input interface

Add support for JSONs as input for TSNsched.

Enable ports with the same name in different switches

TSNsched uses the name of the port to specify some variables to the SMT solver. The solver does not care about the structure of the ports or switches, and if two ports have the same name, there will be multiple variables representing different elements of the network to the solver with the same name as well.

Until this get fixed, please, use unique name to all ports, or do not specify the name of the port at all.

Incompatibilities with latest Z3 releases

It seems that TSNSched has some problems with the latest Z3 releases (4.10 and above)

:./libs/com.microsoft.z3.jar:./libs/gson-2.8.6.jar:./libs/java-json.jar:./libs/TSNsched.jar
java: symbol lookup error: /usr/lib/libz3java.so: undefined symbol: Z3_toggle_warning_messages

Installing Z3 v4.9.1 seems to solve the problem.

Clearly, I also had also to revert the changes for the m1 chip as described in #24

Priorities of different Fragments

Hello,
Why do different fragments of a stream have different priorities?
What determines this priority?
Wasn't the priority of each stream initially defined by the user?
Another question is, Where is the maximum latency that can be tolerated per flow set? I now want to change the maximum latency of a flow, but I can't find the corresponding code.

Consider the interframe gap delay

Currently TSNsched does not consider the interframe gap delay natively, and this must be fixed.

Flows with the same source but different periods

Hey there,
thank you for the nice tool!. While trying to use Tsn-Sched, I noticed that when defining flows of the same source node but with different periods, the resulting model is (most of the time) unsatisfiable (even for a simple topology)
For example, suppose we have the topology :

dev1 --> swt1 --> swt2 --> dev2

and 3 flows f1,f2, and f3 (with periods 250, 500, and 1000 respectively) starting from dev1 and ending at dev2.
Even with the simple setup, the solver does not find any solution, so I would like to learn more about the reason behind the unsatisfiability.

So is there anything wrong with my understanding?
Thank you in advance,
George

P.S: The network of the example is defined as follows:

        ////////////////////////////////////////////
        // defining devices && switches
        ////////////////////////////////////////////
        Device dev1 = new Device(250, 0, 10000000, 250);
        Device dev2 = new Device(250, 0, 10000000, 150);
        TSNSwitch swt1 = new TSNSwitch("swt1", 1500, 1, 250, 1, 1, 200000);
        TSNSwitch swt2 = new TSNSwitch("swt2", 1500, 1, 250, 1, 1, 200000);
        ////////////////////////////////////////////
        // defining Cycles && ports
        ////////////////////////////////////////////
        Cycle c1 = new Cycle(200000);
        Cycle c2 = new Cycle(200000);
        Cycle c3 = new Cycle(200000);
        swt1.createPort(swt2, c1);
        swt1.createPort(dev1, c2);
        swt2.createPort(dev2, c3);
        ////////////////////////////////////////////
        // defining Flows
        ////////////////////////////////////////////
        Flow f1 = new Flow("f1", Flow.PUBLISH_SUBSCRIBE);
        f1.setStartDevice(dev1);
        PathNode root1 = f1.getPathTree().getRoot();
        root1.addChild(swt1);
        PathNode pathNode = f1.getPathTree().searchNode("swt1", root1);
        pathNode.addChild(swt2);
        PathNode pathNode2 = f1.getPathTree().searchNode("swt2", root1);
        pathNode2.addChild(dev2);
        f1.setFixedPriority(true);
        f1.setPriorityValue(7);

        Flow f2 = new Flow("f2", Flow.PUBLISH_SUBSCRIBE);
        f2.setStartDevice(dev1);
        PathNode root2 = f2.getPathTree().getRoot();
        root2.addChild(swt1);
        PathNode pathNode3 = f2.getPathTree().searchNode("swt1", root2);
        pathNode3.addChild(swt2);
        PathNode pathNode4 = f2.getPathTree().searchNode("swt2", root2);
        pathNode4.addChild(dev2);
        f2.setFixedPriority(true);
        f2.setPriorityValue(7);

        Flow f3 = new Flow("f3", Flow.PUBLISH_SUBSCRIBE);
        f3.setStartDevice(dev1);
        PathNode root3 = f3.getPathTree().getRoot();
        root3.addChild(swt1);
        PathNode pathNode5 = f3.getPathTree().searchNode("swt1", root3);
        pathNode5.addChild(swt2);
        PathNode pathNode6 = f3.getPathTree().searchNode("swt2", root3);
        pathNode6.addChild(dev2);
        f3.setFixedPriority(true);
        f3.setPriorityValue(7);
        ////////////////////////////////////////////
        // setting periods for the flows
        ////////////////////////////////////////////
        f1.setFlowSendingPeriodicity(250);
        f2.setFlowSendingPeriodicity(500);
        f3.setFlowSendingPeriodicity(1000);
        ////////////////////////////////////////////
        // Defining network
        ////////////////////////////////////////////
        Network net = new Network();
        net.addDevice(dev2);
        net.addDevice(dev1);
        net.addSwitch(swt2);
        net.addSwitch(swt1);
        net.addFlow(f2);
        net.addFlow(f1);
        net.addFlow(f3);
        
        ////////////////////////////////////////////
        // checking the module
        ////////////////////////////////////////////
        ScheduleGenerator scheduleGenerator = new ScheduleGenerator();
        scheduleGenerator.setEnableLoggerFile(true);
        scheduleGenerator.setEnableConsoleOutput(true);
        scheduleGenerator.generateSchedule(net);