We present our tool output in mvsis format for several case studies and their corresponding schedules

N: number of processes
L: Variables domain size
We denote the schedule by a permutation sch={s1, s2, s3,...,sN} representing the order in which the processes actions have been synthesized by the tool.

Output Format:(follows mvsis output format)

v1,v2,v3... are values
x1, x2, x3 ... are variables



x1{v1,v2,v3} stands for (x1==v1 || x1==v2 || x1==v3)

x1{v1}x2{v2} stands for (x1==v1 && x2==v2)

x1{v1}+x2{v2} stands for (x1==v1 || x2==v2)

{x1}{v1}: (Logic Expression) stands for the guarded command: 
            (Logic Expression --> x1:=v1)


Additions and subtractions are modulo L for variable values and modulo N for variables indices