If using more than 2 TS in the agent model, the guard doesn't work properly.
The problem is that graph product is done iteratively by doing the product of 2 TS at a time, including node generation and building transitions. The guard doesn't work because it is not checked always against the final node label.
One way to solve the issue would be to build all nodes of the product at once, and then only build the transitions.
If using more than 2 TS in the agent model, the guard doesn't work properly.
The problem is that graph product is done iteratively by doing the product of 2 TS at a time, including node generation and building transitions. The guard doesn't work because it is not checked always against the final node label.
One way to solve the issue would be to build all nodes of the product at once, and then only build the transitions.