Benchmark fms.8

Download
model.prism (0.01 MB)
property.props (0.01 MB)
model.jani (0.12 MB)
Origin
Taken from QVBS (January 2026).
The given benchmark (including parameter instantiation and property) has been considered in QComp 2019 and QComp 2020.

Original Prism model and property files have been adapted for compatibility and simplicity:
- Constants: All open constants are now explicitly set within model.prism (no need to set them via command line)
- Properties: The properties only refer to labels and rewards as defined in the model.prism file. No variables or constants are used in the property.
- Formulas: some PRISM formula declarations have been renamed so that their identify does not crash with a label.
Contents of file: model.prism
// flexible manufacturing system [CT93]
// gxn/dxp 11/06/01

ctmc // model is a ctmc

const int n=8; // number of tokens

// rates from Pi equal #(Pi) * min(1, np/r)
// where np = (3n)/2 and r = P1+P2+P3+P12
const int np=floor((3*n)/2);
formula r = P1+P2+P3+P12;

module machine1
	
	P1 : [0..n] init n;
	P1wM1 : [0..n];
	P1M1 : [0..3];
	P1d : [0..n];
	P1s : [0..n];
	P1wP2 : [0..n];
	M1 : [0..3] init 3;   
	
	[t1] (P1>0) & (M1>0) & (P1M1<3)  -> P1*min(1,np/r) : (P1'=P1-1) & (P1M1'=P1M1+1) & (M1'=M1-1);
	[t1] (P1>0) & (M1=0) & (P1wM1 P1*min(1,np/r) : (P1'=P1-1) & (P1wM1'=P1wM1+1);
	
	[] (P1M1>0) & (P1wM1=0) & (M1<3) & (P1s 0.2*P1M1 : (P1M1'=P1M1-1) & (M1'=M1+1) & (P1s'=P1s+1);
	[] (P1M1>0) & (P1wM1>0) & (P1s 0.2*P1M1 : (P1wM1'=P1wM1-1) & (P1s'=P1s+1);
	
	[] (P1M1>0) & (P2wP1=0) & (P1wM1=0) & (M1<3) & (P1wP2 0.05*P1M1 : (P1M1'=P1M1-1) & (M1'=M1+1) & (P1wP2'=P1wP2+1);
	[] (P1M1>0) & (P2wP1=0) & (P1wM1>0) & (P1wP2 0.05*P1M1 : (P1wM1'=P1wM1-1) & (P1wP2'=P1wP2+1);
	
	[p1p2] (P1M1>0) & (P2wP1>0) & (P1wM1=0) & (M1<3) -> 0.05*P1M1 : (P1M1'=P1M1-1) & (M1'=M1+1);
	[p1p2] (P1M1>0) & (P2wP1>0) & (P1wM1>0) -> 0.05*P1M1 : (P1wM1'=P1wM1-1);
	
	[p1p2] (P1wP2>0)  -> 1: (P1wP2'=P1wP2-1);
	[]     (P1s>0) & (P1+P1s<=n) -> 1/60 : (P1s'=0) & (P1'=P1+P1s);
	[fp12] (P1+P12s<=n) -> 1: (P1'=P1+P12s);
	
endmodule

module machine2
	
	P2 : [0..n] init n;
	P2wM2 : [0..n];
	P2M2 : [0..1];
	P2s : [0..n];
	P2wP1 : [0..n];
	M2 : [0..1] init 1;
	
	[t2] (P2>0) & (M2>0) & (P2M2<1)  -> P2*min(1,np/r) : (P2'=P2-1) & (P2M2'=P2M2+1) & (M2'=M2-1);
	[t2] (P2>0) & (M2=0) & (P2wM2 P2*min(1,np/r) : (P2'=P2-1) & (P2wM2'=P2wM2+1);
	
	[] (P2M2>0) & (P2wM2=0) & (M2<1) & (P2s 0.1 : (P2M2'=P2M2-1) & (M2'=M2+1) & (P2s'=P2s+1);
	[] (P2M2>0) & (P2wM2>0) & (P2s 0.1 : (P2wM2'=P2wM2-1) & (P2s'=P2s+1);
	
	[] (P2M2>0) & (P1wP2=0) & (P2wM2=0) & (M2<1) & (P2wP1 1/15: (P2M2'=P2M2-1) & (M2'=M2+1) & (P2wP1'=P2wP1+1);
	[] (P2M2>0) & (P1wP2=0) & (P2wM2>0) & (P2wP1 1/15: (P2wM2'=P2wM2-1) & (P2wP1'=P2wP1+1);
	
	[p1p2] (P2M2>0) & (P1wP2>0) & (P2wM2=0) & (M2<1) -> 1/15: (P2M2'=P2M2-1) & (M2'=M2+1);
	[p1p2] (P2M2>0) & (P1wP2>0) & (P2wM2>0) -> 1/15: (P2wM2'=P2wM2-1);
	
	[p1p2] (P2wP1>0) -> 1 : (P2wP1'=P2wP1-1);
	[]     (P2s>0) & (P2+P2s<=n) -> 1/60 : (P2s'=0) & (P2'=P2+P2s);
	[fp12] (P2+P12s<=n) -> 1 : (P2'=P2+P12s);
	[p2p3] (M2>0) -> 1 : (M2'=M2);
	
endmodule

module machine3 
	
	P3 : [0..n] init n;
	P3M2 : [0..n];
	P3s : [0..n];
	
	[t3] (P3>0) & (P3M2 P3*min(1,np/r) : (P3'=P3-1) & (P3M2'=P3M2+1);
	
	[p2p3] (P3M2>0) & (P3s 1/2 : (P3M2'=P3M2-1) & (P3s'=P3s+1);
	[]     (P3s>0) & (P3+P3s<=n) -> 1/60 : (P3s'=0) & (P3'=P3+P3s);
	
endmodule

module machine12
	
	P12 : [0..n];
	P12wM3 : [0..n];
	P12M3 : [0..2];
	P12s : [0..n];
	M3 : [0..2] init 2;
	
	[p1p2] (P12 1: (P12'=P12+1);
	
	[t12] (P12>0) & (M3>0) & (P12M3<2) -> P12*min(1,np/r) : (P12'=P12-1) & (P12M3'=P12M3+1) & (M3'=M3-1);
	[t12] (P12>0) & (M3=0) & (P12wM3 P12*min(1,np/r) : (P12'=P12-1) & (P12wM3'=P12wM3+1);
	
	[] (P12M3>0) & (P12wM3=0) & (P12s P12M3 : (P12M3'=P12M3-1) & (P12s'=P12s+1) & (M3'=M3+1);
	[] (P12M3>0) & (P12wM3>0) & (P12s P12M3 : (P12wM3'=P12wM3-1) & (P12s'=P12s+1);
	
	[fp12] (P12s>0) -> 1/60 : (P12s'=0);
	
endmodule

// reward structures

// productivity of the system
rewards "productivity"
	[t1]  true : 400;
	[t2]  true : 600;
	[t3]  true : 100;
	[t12] true : 1100;
endrewards
Contents of file: property.props
// Expected productivity of the system
"productivity": R{"productivity"}=? [ S ];
Contents of file: model.jani
{
    "actions": [
        {
            "name": "fp12"
        },
        {
            "name": "p1p2"
        },
        {
            "name": "p2p3"
        },
        {
            "name": "t1"
        },
        {
            "name": "t12"
        },
        {
            "name": "t2"
        },
        {
            "name": "t3"
        }
    ],
    "automata": [
        {
            "edges": [
                {
                    "destinations": [
                        {
                            "assignments": [
                                {
                                    "comment": "P1M1 <- (P1M1 - 1)",
                                    "ref": "P1M1",
                                    "value": {
                                        "left": "P1M1",
                                        "op": "-",
                                        "right": 1
                                    }
                                },
                                {
                                    "comment": "P1s <- (P1s + 1)",
                                    "ref": "P1s",
                                    "value": {
                                        "left": "P1s",
                                        "op": "+",
                                        "right": 1
                                    }
                                },
                                {
                                    "comment": "M1 <- (M1 + 1)",
                                    "ref": "M1",
                                    "value": {
                                        "left": "M1",
                                        "op": "+",
                                        "right": 1
                                    }
                                }
                            ],
                            "location": "l",
                            "probability": {
                                "comment": "((1/5 * P1M1) / (1/5 * P1M1))",
                                "exp": {
                                    "left": {
                                        "left": {
                                            "left": 1.0,
                                            "op": "/",
                                            "right": 5.0
                                        },
                                        "op": "*",
                                        "right": "P1M1"
                                    },
                                    "op": "/",
                                    "right": {
                                        "left": {
                                            "left": 1.0,
                                            "op": "/",
                                            "right": 5.0
                                        },
                                        "op": "*",
                                        "right": "P1M1"
                                    }
                                }
                            }
                        }
                    ],
                    "guard": {
                        "comment": "((((P1M1 > 0) & (P1wM1 = 0)) & (M1 < 3)) & (P1s < 8))",
                        "exp": {
                            "left": {
                                "left": {
                                    "left": "P1s",
                                    "op": "<",
                                    "right": 8
                                },
                                "op": "∧",
                                "right": {
                                    "left": "P1wM1",
                                    "op": "=",
                                    "right": 0
                                }
                            },
                            "op": "∧",
                            "right": {
                                "left": {
                                    "left": "M1",
                                    "op": "<",
                                    "right": 3
                                },
                                "op": "∧",
                                "right": {
                                    "left": "P1M1",
                                    "op": ">",
                                    "right": 0
                                }
                            }
                        }
                    },
                    "location": "l",
                    "rate": {
                        "comment": "(1/5 * P1M1)",
                        "exp": {
                            "left": {
                                "left": 1.0,
                                "op": "/",
                                "right": 5.0
                            },
                            "op": "*",
                            "right": "P1M1"
                        }
                    }
                },
                {
                    "destinations": [
                        {
                            "assignments": [
                                {
                                    "comment": "P1wM1 <- (P1wM1 - 1)",
                                    "ref": "P1wM1",
                                    "value": {
                                        "left": "P1wM1",
                                        "op": "-",
                                        "right": 1
                                    }
                                },
                                {
                                    "comment": "P1s <- (P1s + 1)",
                                    "ref": "P1s",
                                    "value": {
                                        "left": "P1s",
                                        "op": "+",
                                        "right": 1
                                    }
                                }
                            ],
                            "location": "l",
                            "probability": {
                                "comment": "((1/5 * P1M1) / (1/5 * P1M1))",
                                "exp": {
                                    "left": {
                                        "left": {
                                            "left": 1.0,
                                            "op": "/",
                                            "right": 5.0
                                        },
                                        "op": "*",
                                        "right": "P1M1"
                                    },
                                    "op": "/",
                                    "right": {
                                        "left": {
                                            "left": 1.0,
                                            "op": "/",
                                            "right": 5.0
                                        },
                                        "op": "*",
                                        "right": "P1M1"
                                    }
                                }
                            }
                        }
                    ],
                    "guard": {
                        "comment": "(((P1M1 > 0) & (P1wM1 > 0)) & (P1s < 8))",
                        "exp": {
                            "left": {
                                "left": {
                                    "left": "P1M1",
                                    "op": ">",
                                    "right": 0
                                },
                                "op": "∧",
                                "right": {
                                    "left": "P1wM1",
                                    "op": ">",
                                    "right": 0
                                }
                            },
                            "op": "∧",
                            "right": {
                                "left": "P1s",
                                "op": "<",
                                "right": 8
                            }
                        }
                    },
                    "location": "l",
                    "rate": {
                        "comment": "(1/5 * P1M1)",
                        "exp": {
                            "left": {
                                "left": 1.0,
                                "op": "/",
                                "right": 5.0
                            },
                            "op": "*",
                            "right": "P1M1"
                        }
                    }
                },
                {
                    "destinations": [
                        {
                            "assignments": [
                                {
                                    "comment": "P1M1 <- (P1M1 - 1)",
                                    "ref": "P1M1",
                                    "value": {
                                        "left": "P1M1",
                                        "op": "-",
                                        "right": 1
                                    }
                                },
                                {
                                    "comment": "P1wP2 <- (P1wP2 + 1)",
                                    "ref": "P1wP2",
                                    "value": {
                                        "left": "P1wP2",
                                        "op": "+",
                                        "right": 1
                                    }
                                },
                                {
                                    "comment": "M1 <- (M1 + 1)",
                                    "ref": "M1",
                                    "value": {
                                        "left": "M1",
                                        "op": "+",
                                        "right": 1
                                    }
                                }
                            ],
                            "location": "l",
                            "probability": {
                                "comment": "((1/20 * P1M1) / (1/20 * P1M1))",
                                "exp": {
                                    "left": {
                                        "left": {
                                            "left": 1.0,
                                            "op": "/",
                                            "right": 20.0
                                        },
                                        "op": "*",
                                        "right": "P1M1"
                                    },
                                    "op": "/",
                                    "right": {
                                        "left": {
                                            "left": 1.0,
                                            "op": "/",
                                            "right": 20.0
                                        },
                                        "op": "*",
                                        "right": "P1M1"
                                    }
                                }
                            }
                        }
                    ],
                    "guard": {
                        "comment": "(((((P1M1 > 0) & (P2wP1 = 0)) & (P1wM1 = 0)) & (M1 < 3)) & (P1wP2 < 8))",
                        "exp": {
                            "left": {
                                "left": {
                                    "left": {
                                        "left": "P1wP2",
                                        "op": "<",
                                        "right": 8
                                    },
                                    "op": "∧",
                                    "right": {
                                        "left": "P2wP1",
                                        "op": "=",
                                        "right": 0
                                    }
                                },
                                "op": "∧",
                                "right": {
                                    "left": "P1wM1",
                                    "op": "=",
                                    "right": 0
                                }
                            },
                            "op": "∧",
                            "right": {
                                "left": {
                                    "left": "M1",
                                    "op": "<",
                                    "right": 3
                                },
                                "op": "∧",
                                "right": {
                                    "left": "P1M1",
                                    "op": ">",
                                    "right": 0
                                }
                            }
                        }
                    },
                    "location": "l",
                    "rate": {
                        "comment": "(1/20 * P1M1)",
                        "exp": {
                            "left": {
                                "left": 1.0,
                                "op": "/",
                                "right": 20.0
                            },
                            "op": "*",
                            "right": "P1M1"
                        }
                    }
                },
                {
                    "destinations": [
                        {
                            "assignments": [
                                {
                                    "comment": "P1wM1 <- (P1wM1 - 1)",
                                    "ref": "P1wM1",
                                    "value": {
                                        "left": "P1wM1",
                                        "op": "-",
                                        "right": 1
                                    }
                                },
                                {
                                    "comment": "P1wP2 <- (P1wP2 + 1)",
                                    "ref": "P1wP2",
                                    "value": {
                                        "left": "P1wP2",
                                        "op": "+",
                                        "right": 1
                                    }
                                }
                            ],
                            "location": "l",
                            "probability": {
                                "comment": "((1/20 * P1M1) / (1/20 * P1M1))",
                                "exp": {
                                    "left": {
                                        "left": {
                                            "left": 1.0,
                                            "op": "/",
                                            "right": 20.0
                                        },
                                        "op": "*",
                                        "right": "P1M1"
                                    },
                                    "op": "/",
                                    "right": {
                                        "left": {
                                            "left": 1.0,
                                            "op": "/",
                                            "right": 20.0
                                        },
                                        "op": "*",
                                        "right": "P1M1"
                                    }
                                }
                            }
                        }
                    ],
                    "guard": {
                        "comment": "((((P1M1 > 0) & (P2wP1 = 0)) & (P1wM1 > 0)) & (P1wP2 < 8))",
                        "exp": {
                            "left": {
                                "left": {
                                    "left": "P1wP2",
                                    "op": "<",
                                    "right": 8
                                },
                                "op": "∧",
                                "right": {
                                    "left": "P2wP1",
                                    "op": "=",
                                    "right": 0
                                }
                            },
                            "op": "∧",
                            "right": {
                                "left": {
                                    "left": "P1wM1",
                                    "op": ">",
                                    "right": 0
                                },
                                "op": "∧",
                                "right": {
                                    "left": "P1M1",
                                    "op": ">",
                                    "right": 0
                                }
                            }
                        }
                    },
                    "location": "l",
                    "rate": {
                        "comment": "(1/20 * P1M1)",
                        "exp": {
                            "left": {
                                "left": 1.0,
                                "op": "/",
                                "right": 20.0
                            },
                            "op": "*",
                            "right": "P1M1"
                        }
                    }
                },
                {
                    "destinations": [
                        {
                            "assignments": [
                                {
                                    "comment": "P1 <- (P1 + P1s)",
                                    "ref": "P1",
                                    "value": {
                                        "left": "P1",
                                        "op": "+",
                                        "right": "P1s"
                                    }
                                },
                                {
                                    "comment": "P1s <- 0",
                                    "ref": "P1s",
                                    "value": 0
                                }
                            ],
                            "location": "l",
                            "probability": {
                                "comment": "((1 / 60) / (1 / 60))",
                                "exp": {
                                    "left": {
                                        "left": 1,
                                        "op": "/",
                                        "right": 60
                                    },
                                    "op": "/",
                                    "right": {
                                        "left": 1,
                                        "op": "/",
                                        "right": 60
                                    }
                                }
                            }
                        }
                    ],
                    "guard": {
                        "comment": "((P1s > 0) & ((P1 + P1s) <= 8))",
                        "exp": {
                            "left": {
                                "left": "P1s",
                                "op": ">",
                                "right": 0
                            },
                            "op": "∧",
                            "right": {
                                "left": {
                                    "left": "P1",
                                    "op": "+",
                                    "right": "P1s"
                                },
                                "op": "≤",
                                "right": 8
                            }
                        }
                    },
                    "location": "l",
                    "rate": {
                        "comment": "(1 / 60)",
                        "exp": {
                            "left": 1,
                            "op": "/",
                            "right": 60
                        }
                    }
                },
                {
                    "action": "fp12",
                    "destinations": [
                        {
                            "assignments": [
                                {
                                    "comment": "P1 <- (P1 + P12s)",
                                    "ref": "P1",
                                    "value": {
                                        "left": "P1",
                                        "op": "+",
                                        "right": "P12s"
                                    }
                                }
                            ],
                            "location": "l",
                            "probability": {
                                "comment": "(1 / 1)",
                                "exp": 1
                            }
                        }
                    ],
                    "guard": {
                        "comment": "((P1 + P12s) <= 8)",
                        "exp": {
                            "left": {
                                "left": "P1",
                                "op": "+",
                                "right": "P12s"
                            },
                            "op": "≤",
                            "right": 8
                        }
                    },
                    "location": "l",
                    "rate": {
                        "comment": "1",
                        "exp": 1
                    }
                },
                {
                    "action": "p1p2",
                    "destinations": [
                        {
                            "assignments": [
                                {
                                    "comment": "P1M1 <- (P1M1 - 1)",
                                    "ref": "P1M1",
                                    "value": {
                                        "left": "P1M1",
                                        "op": "-",
                                        "right": 1
                                    }
                                },
                                {
                                    "comment": "M1 <- (M1 + 1)",
                                    "ref": "M1",
                                    "value": {
                                        "left": "M1",
                                        "op": "+",
                                        "right": 1
                                    }
                                }
                            ],
                            "location": "l",
                            "probability": {
                                "comment": "((1/20 * P1M1) / (1/20 * P1M1))",
                                "exp": {
                                    "left": {
                                        "left": {
                                            "left": 1.0,
                                            "op": "/",
                                            "right": 20.0
                                        },
                                        "op": "*",
                                        "right": "P1M1"
                                    },
                                    "op": "/",
                                    "right": {
                                        "left": {
                                            "left": 1.0,
                                            "op": "/",
                                            "right": 20.0
                                        },
                                        "op": "*",
                                        "right": "P1M1"
                                    }
                                }
                            }
                        }
                    ],
                    "guard": {
                        "comment": "((((P1M1 > 0) & (P2wP1 > 0)) & (P1wM1 = 0)) & (M1 < 3))",
                        "exp": {
                            "left": {
                                "left": {
                                    "left": "M1",
                                    "op": "<",
                                    "right": 3
                                },
                                "op": "∧",
                                "right": {
                                    "left": "P2wP1",
                                    "op": ">",
                                    "right": 0
                                }
                            },
                            "op": "∧",
                            "right": {
                                "left": {
                                    "left": "P1wM1",
                                    "op": "=",
                                    "right": 0
                                },
                                "op": "∧",
                                "right": {
                                    "left": "P1M1",
                                    "op": ">",
                                    "right": 0
                                }
                            }
                        }
                    },
                    "location": "l",
                    "rate": {
                        "comment": "(1/20 * P1M1)",
                        "exp": {
                            "left": {
                                "left": 1.0,
                                "op": "/",
                                "right": 20.0
                            },
                            "op": "*",
                            "right": "P1M1"
                        }
                    }
                },
                {
                    "action": "p1p2",
                    "destinations": [
                        {
                            "assignments": [
                                {
                                    "comment": "P1wM1 <- (P1wM1 - 1)",
                                    "ref": "P1wM1",
                                    "value": {
                                        "left": "P1wM1",
                                        "op": "-",
                                        "right": 1
                                    }
                                }
                            ],
                            "location": "l",
                            "probability": {
                                "comment": "((1/20 * P1M1) / (1/20 * P1M1))",
                                "exp": {
                                    "left": {
                                        "left": {
                                            "left": 1.0,
                                            "op": "/",
                                            "right": 20.0
                                        },
                                        "op": "*",
                                        "right": "P1M1"
                                    },
                                    "op": "/",
                                    "right": {
                                        "left": {
                                            "left": 1.0,
                                            "op": "/",
                                            "right": 20.0
                                        },
                                        "op": "*",
                                        "right": "P1M1"
                                    }
                                }
                            }
                        }
                    ],
                    "guard": {
                        "comment": "(((P1M1 > 0) & (P2wP1 > 0)) & (P1wM1 > 0))",
                        "exp": {
                            "left": {
                                "left": {
                                    "left": "P1M1",
                                    "op": ">",
                                    "right": 0
                                },
                                "op": "∧",
                                "right": {
                                    "left": "P2wP1",
                                    "op": ">",
                                    "right": 0
                                }
                            },
                            "op": "∧",
                            "right": {
                                "left": "P1wM1",
                                "op": ">",
                                "right": 0
                            }
                        }
                    },
                    "location": "l",
                    "rate": {
                        "comment": "(1/20 * P1M1)",
                        "exp": {
                            "left": {
                                "left": 1.0,
                                "op": "/",
                                "right": 20.0
                            },
                            "op": "*",
                            "right": "P1M1"
                        }
                    }
                },
                {
                    "action": "p1p2",
                    "destinations": [
                        {
                            "assignments": [
                                {
                                    "comment": "P1wP2 <- (P1wP2 - 1)",
                                    "ref": "P1wP2",
                                    "value": {
                                        "left": "P1wP2",
                                        "op": "-",
                                        "right": 1
                                    }
                                }
                            ],
                            "location": "l",
                            "probability": {
                                "comment": "(1 / 1)",
                                "exp": 1
                            }
                        }
                    ],
                    "guard": {
                        "comment": "(P1wP2 > 0)",
                        "exp": {
                            "left": "P1wP2",
                            "op": ">",
                            "right": 0
                        }
                    },
                    "location": "l",
                    "rate": {
                        "comment": "1",
                        "exp": 1
                    }
                },
                {
                    "action": "t1",
                    "destinations": [
                        {
                            "assignments": [
                                {
                                    "comment": "P1 <- (P1 - 1)",
                                    "ref": "P1",
                                    "value": {
                                        "left": "P1",
                                        "op": "-",
                                        "right": 1
                                    }
                                },
                                {
                                    "comment": "P1M1 <- (P1M1 + 1)",
                                    "ref": "P1M1",
                                    "value": {
                                        "left": "P1M1",
                                        "op": "+",
                                        "right": 1
                                    }
                                },
                                {
                                    "comment": "M1 <- (M1 - 1)",
                                    "ref": "M1",
                                    "value": {
                                        "left": "M1",
                                        "op": "-",
                                        "right": 1
                                    }
                                },
                                {
                                    "comment": "productivity <- 400",
                                    "ref": "productivity",
                                    "value": 400
                                }
                            ],
                            "location": "l",
                            "probability": {
                                "comment": "((P1 * (min(1, (floor(((3 * 8) / 2)) / r)))) / (P1 * (min(1, (floor(((3 * 8) / 2)) / r)))))",
                                "exp": {
                                    "left": {
                                        "left": "P1",
                                        "op": "*",
                                        "right": {
                                            "left": 1,
                                            "op": "min",
                                            "right": {
                                                "left": 12,
                                                "op": "/",
                                                "right": {
                                                    "args": [],
                                                    "function": "r",
                                                    "op": "call"
                                                }
                                            }
                                        }
                                    },
                                    "op": "/",
                                    "right": {
                                        "left": "P1",
                                        "op": "*",
                                        "right": {
                                            "left": 1,
                                            "op": "min",
                                            "right": {
                                                "left": 12,
                                                "op": "/",
                                                "right": {
                                                    "args": [],
                                                    "function": "r",
                                                    "op": "call"
                                                }
                                            }
                                        }
                                    }
                                }
                            }
                        }
                    ],
                    "guard": {
                        "comment": "(((P1 > 0) & (M1 > 0)) & (P1M1 < 3))",
                        "exp": {
                            "left": {
                                "left": {
                                    "left": "P1",
                                    "op": ">",
                                    "right": 0
                                },
                                "op": "∧",
                                "right": {
                                    "left": "M1",
                                    "op": ">",
                                    "right": 0
                                }
                            },
                            "op": "∧",
                            "right": {
                                "left": "P1M1",
                                "op": "<",
                                "right": 3
                            }
                        }
                    },
                    "location": "l",
                    "rate": {
                        "comment": "(P1 * (min(1, (floor(((3 * 8) / 2)) / r))))",
                        "exp": {
                            "left": "P1",
                            "op": "*",
                            "right": {
                                "left": 1,
                                "op": "min",
                                "right": {
                                    "left": 12,
                                    "op": "/",
                                    "right": {
                                        "args": [],
                                        "function": "r",
                                        "op": "call"
                                    }
                                }
                            }
                        }
                    }
                },
                {
                    "action": "t1",
                    "destinations": [
                        {
                            "assignments": [
                                {
                                    "comment": "P1 <- (P1 - 1)",
                                    "ref": "P1",
                                    "value": {
                                        "left": "P1",
                                        "op": "-",
                                        "right": 1
                                    }
                                },
                                {
                                    "comment": "P1wM1 <- (P1wM1 + 1)",
                                    "ref": "P1wM1",
                                    "value": {
                                        "left": "P1wM1",
                                        "op": "+",
                                        "right": 1
                                    }
                                },
                                {
                                    "comment": "productivity <- 400",
                                    "ref": "productivity",
                                    "value": 400
                                }
                            ],
                            "location": "l",
                            "probability": {
                                "comment": "((P1 * (min(1, (floor(((3 * 8) / 2)) / r)))) / (P1 * (min(1, (floor(((3 * 8) / 2)) / r)))))",
                                "exp": {
                                    "left": {
                                        "left": "P1",
                                        "op": "*",
                                        "right": {
                                            "left": 1,
                                            "op": "min",
                                            "right": {
                                                "left": 12,
                                                "op": "/",
                                                "right": {
                                                    "args": [],
                                                    "function": "r",
                                                    "op": "call"
                                                }
                                            }
                                        }
                                    },
                                    "op": "/",
                                    "right": {
                                        "left": "P1",
                                        "op": "*",
                                        "right": {
                                            "left": 1,
                                            "op": "min",
                                            "right": {
                                                "left": 12,
                                                "op": "/",
                                                "right": {
                                                    "args": [],
                                                    "function": "r",
                                                    "op": "call"
                                                }
                                            }
                                        }
                                    }
                                }
                            }
                        }
                    ],
                    "guard": {
                        "comment": "(((P1 > 0) & (M1 = 0)) & (P1wM1 < 8))",
                        "exp": {
                            "left": {
                                "left": {
                                    "left": "P1",
                                    "op": ">",
                                    "right": 0
                                },
                                "op": "∧",
                                "right": {
                                    "left": "M1",
                                    "op": "=",
                                    "right": 0
                                }
                            },
                            "op": "∧",
                            "right": {
                                "left": "P1wM1",
                                "op": "<",
                                "right": 8
                            }
                        }
                    },
                    "location": "l",
                    "rate": {
                        "comment": "(P1 * (min(1, (floor(((3 * 8) / 2)) / r))))",
                        "exp": {
                            "left": "P1",
                            "op": "*",
                            "right": {
                                "left": 1,
                                "op": "min",
                                "right": {
                                    "left": 12,
                                    "op": "/",
                                    "right": {
                                        "args": [],
                                        "function": "r",
                                        "op": "call"
                                    }
                                }
                            }
                        }
                    }
                }
            ],
            "initial-locations": [
                "l"
            ],
            "locations": [
                {
                    "name": "l"
                }
            ],
            "name": "machine1",
            "variables": [
                {
                    "initial-value": 0,
                    "name": "P1wM1",
                    "type": {
                        "base": "int",
                        "kind": "bounded",
                        "lower-bound": 0,
                        "upper-bound": 8
                    }
                },
                {
                    "initial-value": 0,
                    "name": "P1M1",
                    "type": {
                        "base": "int",
                        "kind": "bounded",
                        "lower-bound": 0,
                        "upper-bound": 3
                    }
                },
                {
                    "initial-value": 0,
                    "name": "P1d",
                    "type": {
                        "base": "int",
                        "kind": "bounded",
                        "lower-bound": 0,
                        "upper-bound": 8
                    }
                },
                {
                    "initial-value": 0,
                    "name": "P1s",
                    "type": {
                        "base": "int",
                        "kind": "bounded",
                        "lower-bound": 0,
                        "upper-bound": 8
                    }
                },
                {
                    "initial-value": 3,
                    "name": "M1",
                    "type": {
                        "base": "int",
                        "kind": "bounded",
                        "lower-bound": 0,
                        "upper-bound": 3
                    }
                }
            ]
        },
        {
            "edges": [
                {
                    "destinations": [
                        {
                            "assignments": [
                                {
                                    "comment": "P2M2 <- (P2M2 - 1)",
                                    "ref": "P2M2",
                                    "value": {
                                        "left": "P2M2",
                                        "op": "-",
                                        "right": 1
                                    }
                                },
                                {
                                    "comment": "P2s <- (P2s + 1)",
                                    "ref": "P2s",
                                    "value": {
                                        "left": "P2s",
                                        "op": "+",
                                        "right": 1
                                    }
                                },
                                {
                                    "comment": "M2 <- (M2 + 1)",
                                    "ref": "M2",
                                    "value": {
                                        "left": "M2",
                                        "op": "+",
                                        "right": 1
                                    }
                                }
                            ],
                            "location": "l",
                            "probability": {
                                "comment": "(1/10 / 1/10)",
                                "exp": 1.0
                            }
                        }
                    ],
                    "guard": {
                        "comment": "((((P2M2 > 0) & (P2wM2 = 0)) & (M2 < 1)) & (P2s < 8))",
                        "exp": {
                            "left": {
                                "left": {
                                    "left": "P2s",
                                    "op": "<",
                                    "right": 8
                                },
                                "op": "∧",
                                "right": {
                                    "left": "P2wM2",
                                    "op": "=",
                                    "right": 0
                                }
                            },
                            "op": "∧",
                            "right": {
                                "left": {
                                    "left": "M2",
                                    "op": "<",
                                    "right": 1
                                },
                                "op": "∧",
                                "right": {
                                    "left": "P2M2",
                                    "op": ">",
                                    "right": 0
                                }
                            }
                        }
                    },
                    "location": "l",
                    "rate": {
                        "comment": "1/10",
                        "exp": {
                            "left": 1.0,
                            "op": "/",
                            "right": 10.0
                        }
                    }
                },
                {
                    "destinations": [
                        {
                            "assignments": [
                                {
                                    "comment": "P2wM2 <- (P2wM2 - 1)",
                                    "ref": "P2wM2",
                                    "value": {
                                        "left": "P2wM2",
                                        "op": "-",
                                        "right": 1
                                    }
                                },
                                {
                                    "comment": "P2s <- (P2s + 1)",
                                    "ref": "P2s",
                                    "value": {
                                        "left": "P2s",
                                        "op": "+",
                                        "right": 1
                                    }
                                }
                            ],
                            "location": "l",
                            "probability": {
                                "comment": "(1/10 / 1/10)",
                                "exp": 1.0
                            }
                        }
                    ],
                    "guard": {
                        "comment": "(((P2M2 > 0) & (P2wM2 > 0)) & (P2s < 8))",
                        "exp": {
                            "left": {
                                "left": {
                                    "left": "P2M2",
                                    "op": ">",
                                    "right": 0
                                },
                                "op": "∧",
                                "right": {
                                    "left": "P2wM2",
                                    "op": ">",
                                    "right": 0
                                }
                            },
                            "op": "∧",
                            "right": {
                                "left": "P2s",
                                "op": "<",
                                "right": 8
                            }
                        }
                    },
                    "location": "l",
                    "rate": {
                        "comment": "1/10",
                        "exp": {
                            "left": 1.0,
                            "op": "/",
                            "right": 10.0
                        }
                    }
                },
                {
                    "destinations": [
                        {
                            "assignments": [
                                {
                                    "comment": "P2M2 <- (P2M2 - 1)",
                                    "ref": "P2M2",
                                    "value": {
                                        "left": "P2M2",
                                        "op": "-",
                                        "right": 1
                                    }
                                },
                                {
                                    "comment": "P2wP1 <- (P2wP1 + 1)",
                                    "ref": "P2wP1",
                                    "value": {
                                        "left": "P2wP1",
                                        "op": "+",
                                        "right": 1
                                    }
                                },
                                {
                                    "comment": "M2 <- (M2 + 1)",
                                    "ref": "M2",
                                    "value": {
                                        "left": "M2",
                                        "op": "+",
                                        "right": 1
                                    }
                                }
                            ],
                            "location": "l",
                            "probability": {
                                "comment": "((1 / 15) / (1 / 15))",
                                "exp": {
                                    "left": {
                                        "left": 1,
                                        "op": "/",
                                        "right": 15
                                    },
                                    "op": "/",
                                    "right": {
                                        "left": 1,
                                        "op": "/",
                                        "right": 15
                                    }
                                }
                            }
                        }
                    ],
                    "guard": {
                        "comment": "(((((P2M2 > 0) & (P1wP2 = 0)) & (P2wM2 = 0)) & (M2 < 1)) & (P2wP1 < 8))",
                        "exp": {
                            "left": {
                                "left": {
                                    "left": {
                                        "left": "P2wP1",
                                        "op": "<",
                                        "right": 8
                                    },
                                    "op": "∧",
                                    "right": {
                                        "left": "P1wP2",
                                        "op": "=",
                                        "right": 0
                                    }
                                },
                                "op": "∧",
                                "right": {
                                    "left": "P2wM2",
                                    "op": "=",
                                    "right": 0
                                }
                            },
                            "op": "∧",
                            "right": {
                                "left": {
                                    "left": "M2",
                                    "op": "<",
                                    "right": 1
                                },
                                "op": "∧",
                                "right": {
                                    "left": "P2M2",
                                    "op": ">",
                                    "right": 0
                                }
                            }
                        }
                    },
                    "location": "l",
                    "rate": {
                        "comment": "(1 / 15)",
                        "exp": {
                            "left": 1,
                            "op": "/",
                            "right": 15
                        }
                    }
                },
                {
                    "destinations": [
                        {
                            "assignments": [
                                {
                                    "comment": "P2wM2 <- (P2wM2 - 1)",
                                    "ref": "P2wM2",
                                    "value": {
                                        "left": "P2wM2",
                                        "op": "-",
                                        "right": 1
                                    }
                                },
                                {
                                    "comment": "P2wP1 <- (P2wP1 + 1)",
                                    "ref": "P2wP1",
                                    "value": {
                                        "left": "P2wP1",
                                        "op": "+",
                                        "right": 1
                                    }
                                }
                            ],
                            "location": "l",
                            "probability": {
                                "comment": "((1 / 15) / (1 / 15))",
                                "exp": {
                                    "left": {
                                        "left": 1,
                                        "op": "/",
                                        "right": 15
                                    },
                                    "op": "/",
                                    "right": {
                                        "left": 1,
                                        "op": "/",
                                        "right": 15
                                    }
                                }
                            }
                        }
                    ],
                    "guard": {
                        "comment": "((((P2M2 > 0) & (P1wP2 = 0)) & (P2wM2 > 0)) & (P2wP1 < 8))",
                        "exp": {
                            "left": {
                                "left": {
                                    "left": "P2wP1",
                                    "op": "<",
                                    "right": 8
                                },
                                "op": "∧",
                                "right": {
                                    "left": "P1wP2",
                                    "op": "=",
                                    "right": 0
                                }
                            },
                            "op": "∧",
                            "right": {
                                "left": {
                                    "left": "P2wM2",
                                    "op": ">",
                                    "right": 0
                                },
                                "op": "∧",
                                "right": {
                                    "left": "P2M2",
                                    "op": ">",
                                    "right": 0
                                }
                            }
                        }
                    },
                    "location": "l",
                    "rate": {
                        "comment": "(1 / 15)",
                        "exp": {
                            "left": 1,
                            "op": "/",
                            "right": 15
                        }
                    }
                },
                {
                    "destinations": [
                        {
                            "assignments": [
                                {
                                    "comment": "P2 <- (P2 + P2s)",
                                    "ref": "P2",
                                    "value": {
                                        "left": "P2",
                                        "op": "+",
                                        "right": "P2s"
                                    }
                                },
                                {
                                    "comment": "P2s <- 0",
                                    "ref": "P2s",
                                    "value": 0
                                }
                            ],
                            "location": "l",
                            "probability": {
                                "comment": "((1 / 60) / (1 / 60))",
                                "exp": {
                                    "left": {
                                        "left": 1,
                                        "op": "/",
                                        "right": 60
                                    },
                                    "op": "/",
                                    "right": {
                                        "left": 1,
                                        "op": "/",
                                        "right": 60
                                    }
                                }
                            }
                        }
                    ],
                    "guard": {
                        "comment": "((P2s > 0) & ((P2 + P2s) <= 8))",
                        "exp": {
                            "left": {
                                "left": "P2s",
                                "op": ">",
                                "right": 0
                            },
                            "op": "∧",
                            "right": {
                                "left": {
                                    "left": "P2",
                                    "op": "+",
                                    "right": "P2s"
                                },
                                "op": "≤",
                                "right": 8
                            }
                        }
                    },
                    "location": "l",
                    "rate": {
                        "comment": "(1 / 60)",
                        "exp": {
                            "left": 1,
                            "op": "/",
                            "right": 60
                        }
                    }
                },
                {
                    "action": "fp12",
                    "destinations": [
                        {
                            "assignments": [
                                {
                                    "comment": "P2 <- (P2 + P12s)",
                                    "ref": "P2",
                                    "value": {
                                        "left": "P2",
                                        "op": "+",
                                        "right": "P12s"
                                    }
                                }
                            ],
                            "location": "l",
                            "probability": {
                                "comment": "(1 / 1)",
                                "exp": 1
                            }
                        }
                    ],
                    "guard": {
                        "comment": "((P2 + P12s) <= 8)",
                        "exp": {
                            "left": {
                                "left": "P2",
                                "op": "+",
                                "right": "P12s"
                            },
                            "op": "≤",
                            "right": 8
                        }
                    },
                    "location": "l",
                    "rate": {
                        "comment": "1",
                        "exp": 1
                    }
                },
                {
                    "action": "p1p2",
                    "destinations": [
                        {
                            "assignments": [
                                {
                                    "comment": "P2M2 <- (P2M2 - 1)",
                                    "ref": "P2M2",
                                    "value": {
                                        "left": "P2M2",
                                        "op": "-",
                                        "right": 1
                                    }
                                },
                                {
                                    "comment": "M2 <- (M2 + 1)",
                                    "ref": "M2",
                                    "value": {
                                        "left": "M2",
                                        "op": "+",
                                        "right": 1
                                    }
                                }
                            ],
                            "location": "l",
                            "probability": {
                                "comment": "((1 / 15) / (1 / 15))",
                                "exp": {
                                    "left": {
                                        "left": 1,
                                        "op": "/",
                                        "right": 15
                                    },
                                    "op": "/",
                                    "right": {
                                        "left": 1,
                                        "op": "/",
                                        "right": 15
                                    }
                                }
                            }
                        }
                    ],
                    "guard": {
                        "comment": "((((P2M2 > 0) & (P1wP2 > 0)) & (P2wM2 = 0)) & (M2 < 1))",
                        "exp": {
                            "left": {
                                "left": {
                                    "left": "M2",
                                    "op": "<",
                                    "right": 1
                                },
                                "op": "∧",
                                "right": {
                                    "left": "P1wP2",
                                    "op": ">",
                                    "right": 0
                                }
                            },
                            "op": "∧",
                            "right": {
                                "left": {
                                    "left": "P2wM2",
                                    "op": "=",
                                    "right": 0
                                },
                                "op": "∧",
                                "right": {
                                    "left": "P2M2",
                                    "op": ">",
                                    "right": 0
                                }
                            }
                        }
                    },
                    "location": "l",
                    "rate": {
                        "comment": "(1 / 15)",
                        "exp": {
                            "left": 1,
                            "op": "/",
                            "right": 15
                        }
                    }
                },
                {
                    "action": "p1p2",
                    "destinations": [
                        {
                            "assignments": [
                                {
                                    "comment": "P2wM2 <- (P2wM2 - 1)",
                                    "ref": "P2wM2",
                                    "value": {
                                        "left": "P2wM2",
                                        "op": "-",
                                        "right": 1
                                    }
                                }
                            ],
                            "location": "l",
                            "probability": {
                                "comment": "((1 / 15) / (1 / 15))",
                                "exp": {
                                    "left": {
                                        "left": 1,
                                        "op": "/",
                                        "right": 15
                                    },
                                    "op": "/",
                                    "right": {
                                        "left": 1,
                                        "op": "/",
                                        "right": 15
                                    }
                                }
                            }
                        }
                    ],
                    "guard": {
                        "comment": "(((P2M2 > 0) & (P1wP2 > 0)) & (P2wM2 > 0))",
                        "exp": {
                            "left": {
                                "left": {
                                    "left": "P2M2",
                                    "op": ">",
                                    "right": 0
                                },
                                "op": "∧",
                                "right": {
                                    "left": "P1wP2",
                                    "op": ">",
                                    "right": 0
                                }
                            },
                            "op": "∧",
                            "right": {
                                "left": "P2wM2",
                                "op": ">",
                                "right": 0
                            }
                        }
                    },
                    "location": "l",
                    "rate": {
                        "comment": "(1 / 15)",
                        "exp": {
                            "left": 1,
                            "op": "/",
                            "right": 15
                        }
                    }
                },
                {
                    "action": "p1p2",
                    "destinations": [
                        {
                            "assignments": [
                                {
                                    "comment": "P2wP1 <- (P2wP1 - 1)",
                                    "ref": "P2wP1",
                                    "value": {
                                        "left": "P2wP1",
                                        "op": "-",
                                        "right": 1
                                    }
                                }
                            ],
                            "location": "l",
                            "probability": {
                                "comment": "(1 / 1)",
                                "exp": 1
                            }
                        }
                    ],
                    "guard": {
                        "comment": "(P2wP1 > 0)",
                        "exp": {
                            "left": "P2wP1",
                            "op": ">",
                            "right": 0
                        }
                    },
                    "location": "l",
                    "rate": {
                        "comment": "1",
                        "exp": 1
                    }
                },
                {
                    "action": "p2p3",
                    "destinations": [
                        {
                            "assignments": [
                                {
                                    "comment": "M2 <- M2",
                                    "ref": "M2",
                                    "value": "M2"
                                }
                            ],
                            "location": "l",
                            "probability": {
                                "comment": "(1 / 1)",
                                "exp": 1
                            }
                        }
                    ],
                    "guard": {
                        "comment": "(M2 > 0)",
                        "exp": {
                            "left": "M2",
                            "op": ">",
                            "right": 0
                        }
                    },
                    "location": "l",
                    "rate": {
                        "comment": "1",
                        "exp": 1
                    }
                },
                {
                    "action": "t2",
                    "destinations": [
                        {
                            "assignments": [
                                {
                                    "comment": "P2 <- (P2 - 1)",
                                    "ref": "P2",
                                    "value": {
                                        "left": "P2",
                                        "op": "-",
                                        "right": 1
                                    }
                                },
                                {
                                    "comment": "P2M2 <- (P2M2 + 1)",
                                    "ref": "P2M2",
                                    "value": {
                                        "left": "P2M2",
                                        "op": "+",
                                        "right": 1
                                    }
                                },
                                {
                                    "comment": "M2 <- (M2 - 1)",
                                    "ref": "M2",
                                    "value": {
                                        "left": "M2",
                                        "op": "-",
                                        "right": 1
                                    }
                                },
                                {
                                    "comment": "productivity <- 600",
                                    "ref": "productivity",
                                    "value": 600
                                }
                            ],
                            "location": "l",
                            "probability": {
                                "comment": "((P2 * (min(1, (floor(((3 * 8) / 2)) / r)))) / (P2 * (min(1, (floor(((3 * 8) / 2)) / r)))))",
                                "exp": {
                                    "left": {
                                        "left": "P2",
                                        "op": "*",
                                        "right": {
                                            "left": 1,
                                            "op": "min",
                                            "right": {
                                                "left": 12,
                                                "op": "/",
                                                "right": {
                                                    "args": [],
                                                    "function": "r",
                                                    "op": "call"
                                                }
                                            }
                                        }
                                    },
                                    "op": "/",
                                    "right": {
                                        "left": "P2",
                                        "op": "*",
                                        "right": {
                                            "left": 1,
                                            "op": "min",
                                            "right": {
                                                "left": 12,
                                                "op": "/",
                                                "right": {
                                                    "args": [],
                                                    "function": "r",
                                                    "op": "call"
                                                }
                                            }
                                        }
                                    }
                                }
                            }
                        }
                    ],
                    "guard": {
                        "comment": "(((P2 > 0) & (M2 > 0)) & (P2M2 < 1))",
                        "exp": {
                            "left": {
                                "left": {
                                    "left": "P2",
                                    "op": ">",
                                    "right": 0
                                },
                                "op": "∧",
                                "right": {
                                    "left": "M2",
                                    "op": ">",
                                    "right": 0
                                }
                            },
                            "op": "∧",
                            "right": {
                                "left": "P2M2",
                                "op": "<",
                                "right": 1
                            }
                        }
                    },
                    "location": "l",
                    "rate": {
                        "comment": "(P2 * (min(1, (floor(((3 * 8) / 2)) / r))))",
                        "exp": {
                            "left": "P2",
                            "op": "*",
                            "right": {
                                "left": 1,
                                "op": "min",
                                "right": {
                                    "left": 12,
                                    "op": "/",
                                    "right": {
                                        "args": [],
                                        "function": "r",
                                        "op": "call"
                                    }
                                }
                            }
                        }
                    }
                },
                {
                    "action": "t2",
                    "destinations": [
                        {
                            "assignments": [
                                {
                                    "comment": "P2 <- (P2 - 1)",
                                    "ref": "P2",
                                    "value": {
                                        "left": "P2",
                                        "op": "-",
                                        "right": 1
                                    }
                                },
                                {
                                    "comment": "P2wM2 <- (P2wM2 + 1)",
                                    "ref": "P2wM2",
                                    "value": {
                                        "left": "P2wM2",
                                        "op": "+",
                                        "right": 1
                                    }
                                },
                                {
                                    "comment": "productivity <- 600",
                                    "ref": "productivity",
                                    "value": 600
                                }
                            ],
                            "location": "l",
                            "probability": {
                                "comment": "((P2 * (min(1, (floor(((3 * 8) / 2)) / r)))) / (P2 * (min(1, (floor(((3 * 8) / 2)) / r)))))",
                                "exp": {
                                    "left": {
                                        "left": "P2",
                                        "op": "*",
                                        "right": {
                                            "left": 1,
                                            "op": "min",
                                            "right": {
                                                "left": 12,
                                                "op": "/",
                                                "right": {
                                                    "args": [],
                                                    "function": "r",
                                                    "op": "call"
                                                }
                                            }
                                        }
                                    },
                                    "op": "/",
                                    "right": {
                                        "left": "P2",
                                        "op": "*",
                                        "right": {
                                            "left": 1,
                                            "op": "min",
                                            "right": {
                                                "left": 12,
                                                "op": "/",
                                                "right": {
                                                    "args": [],
                                                    "function": "r",
                                                    "op": "call"
                                                }
                                            }
                                        }
                                    }
                                }
                            }
                        }
                    ],
                    "guard": {
                        "comment": "(((P2 > 0) & (M2 = 0)) & (P2wM2 < 8))",
                        "exp": {
                            "left": {
                                "left": {
                                    "left": "P2",
                                    "op": ">",
                                    "right": 0
                                },
                                "op": "∧",
                                "right": {
                                    "left": "M2",
                                    "op": "=",
                                    "right": 0
                                }
                            },
                            "op": "∧",
                            "right": {
                                "left": "P2wM2",
                                "op": "<",
                                "right": 8
                            }
                        }
                    },
                    "location": "l",
                    "rate": {
                        "comment": "(P2 * (min(1, (floor(((3 * 8) / 2)) / r))))",
                        "exp": {
                            "left": "P2",
                            "op": "*",
                            "right": {
                                "left": 1,
                                "op": "min",
                                "right": {
                                    "left": 12,
                                    "op": "/",
                                    "right": {
                                        "args": [],
                                        "function": "r",
                                        "op": "call"
                                    }
                                }
                            }
                        }
                    }
                }
            ],
            "initial-locations": [
                "l"
            ],
            "locations": [
                {
                    "name": "l"
                }
            ],
            "name": "machine2",
            "variables": [
                {
                    "initial-value": 0,
                    "name": "P2wM2",
                    "type": {
                        "base": "int",
                        "kind": "bounded",
                        "lower-bound": 0,
                        "upper-bound": 8
                    }
                },
                {
                    "initial-value": 0,
                    "name": "P2M2",
                    "type": {
                        "base": "int",
                        "kind": "bounded",
                        "lower-bound": 0,
                        "upper-bound": 1
                    }
                },
                {
                    "initial-value": 0,
                    "name": "P2s",
                    "type": {
                        "base": "int",
                        "kind": "bounded",
                        "lower-bound": 0,
                        "upper-bound": 8
                    }
                },
                {
                    "initial-value": 1,
                    "name": "M2",
                    "type": {
                        "base": "int",
                        "kind": "bounded",
                        "lower-bound": 0,
                        "upper-bound": 1
                    }
                }
            ]
        },
        {
            "edges": [
                {
                    "destinations": [
                        {
                            "assignments": [
                                {
                                    "comment": "P3 <- (P3 + P3s)",
                                    "ref": "P3",
                                    "value": {
                                        "left": "P3",
                                        "op": "+",
                                        "right": "P3s"
                                    }
                                },
                                {
                                    "comment": "P3s <- 0",
                                    "ref": "P3s",
                                    "value": 0
                                }
                            ],
                            "location": "l",
                            "probability": {
                                "comment": "((1 / 60) / (1 / 60))",
                                "exp": {
                                    "left": {
                                        "left": 1,
                                        "op": "/",
                                        "right": 60
                                    },
                                    "op": "/",
                                    "right": {
                                        "left": 1,
                                        "op": "/",
                                        "right": 60
                                    }
                                }
                            }
                        }
                    ],
                    "guard": {
                        "comment": "((P3s > 0) & ((P3 + P3s) <= 8))",
                        "exp": {
                            "left": {
                                "left": "P3s",
                                "op": ">",
                                "right": 0
                            },
                            "op": "∧",
                            "right": {
                                "left": {
                                    "left": "P3",
                                    "op": "+",
                                    "right": "P3s"
                                },
                                "op": "≤",
                                "right": 8
                            }
                        }
                    },
                    "location": "l",
                    "rate": {
                        "comment": "(1 / 60)",
                        "exp": {
                            "left": 1,
                            "op": "/",
                            "right": 60
                        }
                    }
                },
                {
                    "action": "p2p3",
                    "destinations": [
                        {
                            "assignments": [
                                {
                                    "comment": "P3M2 <- (P3M2 - 1)",
                                    "ref": "P3M2",
                                    "value": {
                                        "left": "P3M2",
                                        "op": "-",
                                        "right": 1
                                    }
                                },
                                {
                                    "comment": "P3s <- (P3s + 1)",
                                    "ref": "P3s",
                                    "value": {
                                        "left": "P3s",
                                        "op": "+",
                                        "right": 1
                                    }
                                }
                            ],
                            "location": "l",
                            "probability": {
                                "comment": "((1 / 2) / (1 / 2))",
                                "exp": {
                                    "left": {
                                        "left": 1,
                                        "op": "/",
                                        "right": 2
                                    },
                                    "op": "/",
                                    "right": {
                                        "left": 1,
                                        "op": "/",
                                        "right": 2
                                    }
                                }
                            }
                        }
                    ],
                    "guard": {
                        "comment": "((P3M2 > 0) & (P3s < 8))",
                        "exp": {
                            "left": {
                                "left": "P3M2",
                                "op": ">",
                                "right": 0
                            },
                            "op": "∧",
                            "right": {
                                "left": "P3s",
                                "op": "<",
                                "right": 8
                            }
                        }
                    },
                    "location": "l",
                    "rate": {
                        "comment": "(1 / 2)",
                        "exp": {
                            "left": 1,
                            "op": "/",
                            "right": 2
                        }
                    }
                },
                {
                    "action": "t3",
                    "destinations": [
                        {
                            "assignments": [
                                {
                                    "comment": "P3 <- (P3 - 1)",
                                    "ref": "P3",
                                    "value": {
                                        "left": "P3",
                                        "op": "-",
                                        "right": 1
                                    }
                                },
                                {
                                    "comment": "P3M2 <- (P3M2 + 1)",
                                    "ref": "P3M2",
                                    "value": {
                                        "left": "P3M2",
                                        "op": "+",
                                        "right": 1
                                    }
                                },
                                {
                                    "comment": "productivity <- 100",
                                    "ref": "productivity",
                                    "value": 100
                                }
                            ],
                            "location": "l",
                            "probability": {
                                "comment": "((P3 * (min(1, (floor(((3 * 8) / 2)) / r)))) / (P3 * (min(1, (floor(((3 * 8) / 2)) / r)))))",
                                "exp": {
                                    "left": {
                                        "left": "P3",
                                        "op": "*",
                                        "right": {
                                            "left": 1,
                                            "op": "min",
                                            "right": {
                                                "left": 12,
                                                "op": "/",
                                                "right": {
                                                    "args": [],
                                                    "function": "r",
                                                    "op": "call"
                                                }
                                            }
                                        }
                                    },
                                    "op": "/",
                                    "right": {
                                        "left": "P3",
                                        "op": "*",
                                        "right": {
                                            "left": 1,
                                            "op": "min",
                                            "right": {
                                                "left": 12,
                                                "op": "/",
                                                "right": {
                                                    "args": [],
                                                    "function": "r",
                                                    "op": "call"
                                                }
                                            }
                                        }
                                    }
                                }
                            }
                        }
                    ],
                    "guard": {
                        "comment": "((P3 > 0) & (P3M2 < 8))",
                        "exp": {
                            "left": {
                                "left": "P3",
                                "op": ">",
                                "right": 0
                            },
                            "op": "∧",
                            "right": {
                                "left": "P3M2",
                                "op": "<",
                                "right": 8
                            }
                        }
                    },
                    "location": "l",
                    "rate": {
                        "comment": "(P3 * (min(1, (floor(((3 * 8) / 2)) / r))))",
                        "exp": {
                            "left": "P3",
                            "op": "*",
                            "right": {
                                "left": 1,
                                "op": "min",
                                "right": {
                                    "left": 12,
                                    "op": "/",
                                    "right": {
                                        "args": [],
                                        "function": "r",
                                        "op": "call"
                                    }
                                }
                            }
                        }
                    }
                }
            ],
            "initial-locations": [
                "l"
            ],
            "locations": [
                {
                    "name": "l"
                }
            ],
            "name": "machine3",
            "variables": [
                {
                    "initial-value": 0,
                    "name": "P3M2",
                    "type": {
                        "base": "int",
                        "kind": "bounded",
                        "lower-bound": 0,
                        "upper-bound": 8
                    }
                },
                {
                    "initial-value": 0,
                    "name": "P3s",
                    "type": {
                        "base": "int",
                        "kind": "bounded",
                        "lower-bound": 0,
                        "upper-bound": 8
                    }
                }
            ]
        },
        {
            "edges": [
                {
                    "destinations": [
                        {
                            "assignments": [
                                {
                                    "comment": "P12M3 <- (P12M3 - 1)",
                                    "ref": "P12M3",
                                    "value": {
                                        "left": "P12M3",
                                        "op": "-",
                                        "right": 1
                                    }
                                },
                                {
                                    "comment": "P12s <- (P12s + 1)",
                                    "ref": "P12s",
                                    "value": {
                                        "left": "P12s",
                                        "op": "+",
                                        "right": 1
                                    }
                                },
                                {
                                    "comment": "M3 <- (M3 + 1)",
                                    "ref": "M3",
                                    "value": {
                                        "left": "M3",
                                        "op": "+",
                                        "right": 1
                                    }
                                }
                            ],
                            "location": "l",
                            "probability": {
                                "comment": "(P12M3 / P12M3)",
                                "exp": {
                                    "left": "P12M3",
                                    "op": "/",
                                    "right": "P12M3"
                                }
                            }
                        }
                    ],
                    "guard": {
                        "comment": "((((P12M3 > 0) & (P12wM3 = 0)) & (P12s < 8)) & (M3 < 2))",
                        "exp": {
                            "left": {
                                "left": {
                                    "left": "M3",
                                    "op": "<",
                                    "right": 2
                                },
                                "op": "∧",
                                "right": {
                                    "left": "P12wM3",
                                    "op": "=",
                                    "right": 0
                                }
                            },
                            "op": "∧",
                            "right": {
                                "left": {
                                    "left": "P12s",
                                    "op": "<",
                                    "right": 8
                                },
                                "op": "∧",
                                "right": {
                                    "left": "P12M3",
                                    "op": ">",
                                    "right": 0
                                }
                            }
                        }
                    },
                    "location": "l",
                    "rate": {
                        "comment": "P12M3",
                        "exp": "P12M3"
                    }
                },
                {
                    "destinations": [
                        {
                            "assignments": [
                                {
                                    "comment": "P12wM3 <- (P12wM3 - 1)",
                                    "ref": "P12wM3",
                                    "value": {
                                        "left": "P12wM3",
                                        "op": "-",
                                        "right": 1
                                    }
                                },
                                {
                                    "comment": "P12s <- (P12s + 1)",
                                    "ref": "P12s",
                                    "value": {
                                        "left": "P12s",
                                        "op": "+",
                                        "right": 1
                                    }
                                }
                            ],
                            "location": "l",
                            "probability": {
                                "comment": "(P12M3 / P12M3)",
                                "exp": {
                                    "left": "P12M3",
                                    "op": "/",
                                    "right": "P12M3"
                                }
                            }
                        }
                    ],
                    "guard": {
                        "comment": "(((P12M3 > 0) & (P12wM3 > 0)) & (P12s < 8))",
                        "exp": {
                            "left": {
                                "left": {
                                    "left": "P12M3",
                                    "op": ">",
                                    "right": 0
                                },
                                "op": "∧",
                                "right": {
                                    "left": "P12wM3",
                                    "op": ">",
                                    "right": 0
                                }
                            },
                            "op": "∧",
                            "right": {
                                "left": "P12s",
                                "op": "<",
                                "right": 8
                            }
                        }
                    },
                    "location": "l",
                    "rate": {
                        "comment": "P12M3",
                        "exp": "P12M3"
                    }
                },
                {
                    "action": "fp12",
                    "destinations": [
                        {
                            "assignments": [
                                {
                                    "comment": "P12s <- 0",
                                    "ref": "P12s",
                                    "value": 0
                                }
                            ],
                            "location": "l",
                            "probability": {
                                "comment": "((1 / 60) / (1 / 60))",
                                "exp": {
                                    "left": {
                                        "left": 1,
                                        "op": "/",
                                        "right": 60
                                    },
                                    "op": "/",
                                    "right": {
                                        "left": 1,
                                        "op": "/",
                                        "right": 60
                                    }
                                }
                            }
                        }
                    ],
                    "guard": {
                        "comment": "(P12s > 0)",
                        "exp": {
                            "left": "P12s",
                            "op": ">",
                            "right": 0
                        }
                    },
                    "location": "l",
                    "rate": {
                        "comment": "(1 / 60)",
                        "exp": {
                            "left": 1,
                            "op": "/",
                            "right": 60
                        }
                    }
                },
                {
                    "action": "p1p2",
                    "destinations": [
                        {
                            "assignments": [
                                {
                                    "comment": "P12 <- (P12 + 1)",
                                    "ref": "P12",
                                    "value": {
                                        "left": "P12",
                                        "op": "+",
                                        "right": 1
                                    }
                                }
                            ],
                            "location": "l",
                            "probability": {
                                "comment": "(1 / 1)",
                                "exp": 1
                            }
                        }
                    ],
                    "guard": {
                        "comment": "(P12 < 8)",
                        "exp": {
                            "left": "P12",
                            "op": "<",
                            "right": 8
                        }
                    },
                    "location": "l",
                    "rate": {
                        "comment": "1",
                        "exp": 1
                    }
                },
                {
                    "action": "t12",
                    "destinations": [
                        {
                            "assignments": [
                                {
                                    "comment": "P12 <- (P12 - 1)",
                                    "ref": "P12",
                                    "value": {
                                        "left": "P12",
                                        "op": "-",
                                        "right": 1
                                    }
                                },
                                {
                                    "comment": "P12M3 <- (P12M3 + 1)",
                                    "ref": "P12M3",
                                    "value": {
                                        "left": "P12M3",
                                        "op": "+",
                                        "right": 1
                                    }
                                },
                                {
                                    "comment": "M3 <- (M3 - 1)",
                                    "ref": "M3",
                                    "value": {
                                        "left": "M3",
                                        "op": "-",
                                        "right": 1
                                    }
                                },
                                {
                                    "comment": "productivity <- 1100",
                                    "ref": "productivity",
                                    "value": 1100
                                }
                            ],
                            "location": "l",
                            "probability": {
                                "comment": "((P12 * (min(1, (floor(((3 * 8) / 2)) / r)))) / (P12 * (min(1, (floor(((3 * 8) / 2)) / r)))))",
                                "exp": {
                                    "left": {
                                        "left": "P12",
                                        "op": "*",
                                        "right": {
                                            "left": 1,
                                            "op": "min",
                                            "right": {
                                                "left": 12,
                                                "op": "/",
                                                "right": {
                                                    "args": [],
                                                    "function": "r",
                                                    "op": "call"
                                                }
                                            }
                                        }
                                    },
                                    "op": "/",
                                    "right": {
                                        "left": "P12",
                                        "op": "*",
                                        "right": {
                                            "left": 1,
                                            "op": "min",
                                            "right": {
                                                "left": 12,
                                                "op": "/",
                                                "right": {
                                                    "args": [],
                                                    "function": "r",
                                                    "op": "call"
                                                }
                                            }
                                        }
                                    }
                                }
                            }
                        }
                    ],
                    "guard": {
                        "comment": "(((P12 > 0) & (M3 > 0)) & (P12M3 < 2))",
                        "exp": {
                            "left": {
                                "left": {
                                    "left": "P12",
                                    "op": ">",
                                    "right": 0
                                },
                                "op": "∧",
                                "right": {
                                    "left": "M3",
                                    "op": ">",
                                    "right": 0
                                }
                            },
                            "op": "∧",
                            "right": {
                                "left": "P12M3",
                                "op": "<",
                                "right": 2
                            }
                        }
                    },
                    "location": "l",
                    "rate": {
                        "comment": "(P12 * (min(1, (floor(((3 * 8) / 2)) / r))))",
                        "exp": {
                            "left": "P12",
                            "op": "*",
                            "right": {
                                "left": 1,
                                "op": "min",
                                "right": {
                                    "left": 12,
                                    "op": "/",
                                    "right": {
                                        "args": [],
                                        "function": "r",
                                        "op": "call"
                                    }
                                }
                            }
                        }
                    }
                },
                {
                    "action": "t12",
                    "destinations": [
                        {
                            "assignments": [
                                {
                                    "comment": "P12 <- (P12 - 1)",
                                    "ref": "P12",
                                    "value": {
                                        "left": "P12",
                                        "op": "-",
                                        "right": 1
                                    }
                                },
                                {
                                    "comment": "P12wM3 <- (P12wM3 + 1)",
                                    "ref": "P12wM3",
                                    "value": {
                                        "left": "P12wM3",
                                        "op": "+",
                                        "right": 1
                                    }
                                },
                                {
                                    "comment": "productivity <- 1100",
                                    "ref": "productivity",
                                    "value": 1100
                                }
                            ],
                            "location": "l",
                            "probability": {
                                "comment": "((P12 * (min(1, (floor(((3 * 8) / 2)) / r)))) / (P12 * (min(1, (floor(((3 * 8) / 2)) / r)))))",
                                "exp": {
                                    "left": {
                                        "left": "P12",
                                        "op": "*",
                                        "right": {
                                            "left": 1,
                                            "op": "min",
                                            "right": {
                                                "left": 12,
                                                "op": "/",
                                                "right": {
                                                    "args": [],
                                                    "function": "r",
                                                    "op": "call"
                                                }
                                            }
                                        }
                                    },
                                    "op": "/",
                                    "right": {
                                        "left": "P12",
                                        "op": "*",
                                        "right": {
                                            "left": 1,
                                            "op": "min",
                                            "right": {
                                                "left": 12,
                                                "op": "/",
                                                "right": {
                                                    "args": [],
                                                    "function": "r",
                                                    "op": "call"
                                                }
                                            }
                                        }
                                    }
                                }
                            }
                        }
                    ],
                    "guard": {
                        "comment": "(((P12 > 0) & (M3 = 0)) & (P12wM3 < 8))",
                        "exp": {
                            "left": {
                                "left": {
                                    "left": "P12",
                                    "op": ">",
                                    "right": 0
                                },
                                "op": "∧",
                                "right": {
                                    "left": "M3",
                                    "op": "=",
                                    "right": 0
                                }
                            },
                            "op": "∧",
                            "right": {
                                "left": "P12wM3",
                                "op": "<",
                                "right": 8
                            }
                        }
                    },
                    "location": "l",
                    "rate": {
                        "comment": "(P12 * (min(1, (floor(((3 * 8) / 2)) / r))))",
                        "exp": {
                            "left": "P12",
                            "op": "*",
                            "right": {
                                "left": 1,
                                "op": "min",
                                "right": {
                                    "left": 12,
                                    "op": "/",
                                    "right": {
                                        "args": [],
                                        "function": "r",
                                        "op": "call"
                                    }
                                }
                            }
                        }
                    }
                }
            ],
            "initial-locations": [
                "l"
            ],
            "locations": [
                {
                    "name": "l"
                }
            ],
            "name": "machine12",
            "variables": [
                {
                    "initial-value": 0,
                    "name": "P12wM3",
                    "type": {
                        "base": "int",
                        "kind": "bounded",
                        "lower-bound": 0,
                        "upper-bound": 8
                    }
                },
                {
                    "initial-value": 0,
                    "name": "P12M3",
                    "type": {
                        "base": "int",
                        "kind": "bounded",
                        "lower-bound": 0,
                        "upper-bound": 2
                    }
                },
                {
                    "initial-value": 2,
                    "name": "M3",
                    "type": {
                        "base": "int",
                        "kind": "bounded",
                        "lower-bound": 0,
                        "upper-bound": 2
                    }
                }
            ]
        }
    ],
    "constants": [
        {
            "name": "n",
            "type": "int",
            "value": 8
        },
        {
            "name": "np",
            "type": "int",
            "value": 12
        }
    ],
    "features": [
        "derived-operators",
        "functions"
    ],
    "functions": [
        {
            "body": {
                "left": {
                    "left": "P12",
                    "op": "+",
                    "right": "P2"
                },
                "op": "+",
                "right": {
                    "left": "P3",
                    "op": "+",
                    "right": "P1"
                }
            },
            "name": "r",
            "parameters": [],
            "type": "int"
        }
    ],
    "jani-version": 1,
    "name": "model",
    "properties": [
        {
            "expression": {
                "fun": "values",
                "op": "filter",
                "states": {
                    "op": "initial"
                },
                "values": {
                    "accumulate": [
                        "steps"
                    ],
                    "exp": "productivity",
                    "op": "Smin"
                }
            },
            "name": "productivity"
        }
    ],
    "restrict-initial": {
        "exp": true
    },
    "system": {
        "elements": [
            {
                "automaton": "machine1"
            },
            {
                "automaton": "machine2"
            },
            {
                "automaton": "machine3"
            },
            {
                "automaton": "machine12"
            }
        ],
        "syncs": [
            {
                "result": "fp12",
                "synchronise": [
                    "fp12",
                    "fp12",
                    null,
                    "fp12"
                ]
            },
            {
                "result": "p1p2",
                "synchronise": [
                    "p1p2",
                    "p1p2",
                    null,
                    "p1p2"
                ]
            },
            {
                "result": "p2p3",
                "synchronise": [
                    null,
                    "p2p3",
                    "p2p3",
                    null
                ]
            },
            {
                "result": "t1",
                "synchronise": [
                    "t1",
                    null,
                    null,
                    null
                ]
            },
            {
                "result": "t12",
                "synchronise": [
                    null,
                    null,
                    null,
                    "t12"
                ]
            },
            {
                "result": "t2",
                "synchronise": [
                    null,
                    "t2",
                    null,
                    null
                ]
            },
            {
                "result": "t3",
                "synchronise": [
                    null,
                    null,
                    "t3",
                    null
                ]
            }
        ]
    },
    "type": "ctmc",
    "variables": [
        {
            "initial-value": 0.0,
            "name": "productivity",
            "transient": true,
            "type": "real"
        },
        {
            "initial-value": 8,
            "name": "P1",
            "type": {
                "base": "int",
                "kind": "bounded",
                "lower-bound": 0,
                "upper-bound": 8
            }
        },
        {
            "initial-value": 0,
            "name": "P1wP2",
            "type": {
                "base": "int",
                "kind": "bounded",
                "lower-bound": 0,
                "upper-bound": 8
            }
        },
        {
            "initial-value": 8,
            "name": "P2",
            "type": {
                "base": "int",
                "kind": "bounded",
                "lower-bound": 0,
                "upper-bound": 8
            }
        },
        {
            "initial-value": 0,
            "name": "P2wP1",
            "type": {
                "base": "int",
                "kind": "bounded",
                "lower-bound": 0,
                "upper-bound": 8
            }
        },
        {
            "initial-value": 8,
            "name": "P3",
            "type": {
                "base": "int",
                "kind": "bounded",
                "lower-bound": 0,
                "upper-bound": 8
            }
        },
        {
            "initial-value": 0,
            "name": "P12",
            "type": {
                "base": "int",
                "kind": "bounded",
                "lower-bound": 0,
                "upper-bound": 8
            }
        },
        {
            "initial-value": 0,
            "name": "P12s",
            "type": {
                "base": "int",
                "kind": "bounded",
                "lower-bound": 0,
                "upper-bound": 8
            }
        }
    ]
}