parametric systems lecture - RWTH Aachen University

Parameter Synthesis in Markov Chains: The Why and How?

Sebastian Junges

Including work with and by: Erika Abraham, Christel Baier, Bernd Becker, Harold Bruintjes, Florian Corzilius, Murat Cubuktepe, Christian Dehnert, Nils Jansen, Joost-Pieter Katoen, Joachim Klein, Lisa Hutschenreiter, Ufuk Topcu, Tim Quatmann, Matthias Volk, Leonore Winterer, Ralf Wimmer

Last Lecture Modelling and Verification of Probabilistic Systems

Parameter Synthesis in Markov Chains Modelling and Verification of Probabilistic Systems Sebastian Junges

parametric Markov Chains (pMCs)

!2

s1

s3 s4

s2 s5

s6 s7

12

12

12

12

12

12

12

12

12

12

12

12

12

12

Knuth-Yao Die


Knuth-Yao Die

!3

s1

s3 s4

s2 s5

s6 s7

12

12

12

12

12

12

12

12

12

12

12

12

12

12

16

16

16

16

16

16


Knuth-Yao Die

!4

s1

s3 s4

s2 s5

s6 s7

12

12

12

12

0.48 0.52

0.52 0.52 0.52 0.52

0.48 0.48

0.48 0.48

0.164… 0.164… 0.151… 0.178… 0.178… 0.164…


Knuth-Yao Die

!5

s1

s3 s4

s2 s5

s6 s7

0.48 0.52

0.52 0.52 0.52 0.52

0.48 0.48

0.48 0.48

?

0.40.4

0.6 0.6

? ? ? ? ?


Knuth-Yao Die

!6

s1

s3 s4

s2 s5

s6 s7

p

p p

pp

q q

1�q 1�q

1�p

1�p 1�p 1�p 1�p


Self-stabilizing algorithms

A distributed system is self-stabilizing iff it satisfies:

1. Convergence (recovery): Starting from any arbitrary state, it always reaches a legitimate state in a finite number of steps, and

2. Closure: It remains in legitimate states in the absence of faults

!7

Legitimate states

State space

X


Herman’s randomized self-stabilizing algorithm

!8

p0

p3p2

p4p1

1

0

1

1

0

xi 6= xi�1 ! xi := xi�1<latexit sha1_base64="tdLIqvvWZ5dCisSXvHjOp73tm0A=">AAAC9XichVFNSxxBEH1OEr8SzSY55jK4BALBZSYEogFBEiO5CApuFFxZesZ2bHZ2Zuzp1d0s+yP8A54k1xy9Jj8j/hYPed2ZDUQRe+ip6levXld1RUWqShMEvye8Bw8fTU5Nz8w+fjI3/7T27PnXMu/pWDbjPM31biRKmapMNo0yqdwttBTdKJU7UeeTje+cSF2qPNs2g0Lud0WSqUMVC0OoXXvTbyu/lcljv98eqsVw5Le0So6M0Do/9W3ww8o41K7Vg0bgln/bCSunjmpt5rUrtHCAHDF66EIig6GfQqDkt4cQAQpi+xgS0/SUi0uMMMvcHlmSDEG0w3/C016FZjxbzdJlx7wl5dbM9PGKe90pRmTbWyX9kvaa+5vDkjtvGDplW+GANqLijFPcIG5wRMZ9md2KOa7l/kzblcEhllw3ivUVDrF9xv901hjRxDou4uOzYybUiNz5hC+Q0TZZgX3lsYLvOj6gFc5Kp5JVioJ6mta+PuvhmMObQ73tNN82lhvh1rv66sdq3tN4iQW85lDfYxVfsMkyYpzhEj/xy+t7596F9/0v1Zuocl7gv+X9+AO6pZ9i</latexit><latexit sha1_base64="tdLIqvvWZ5dCisSXvHjOp73tm0A=">AAAC9XichVFNSxxBEH1OEr8SzSY55jK4BALBZSYEogFBEiO5CApuFFxZesZ2bHZ2Zuzp1d0s+yP8A54k1xy9Jj8j/hYPed2ZDUQRe+ip6levXld1RUWqShMEvye8Bw8fTU5Nz8w+fjI3/7T27PnXMu/pWDbjPM31biRKmapMNo0yqdwttBTdKJU7UeeTje+cSF2qPNs2g0Lud0WSqUMVC0OoXXvTbyu/lcljv98eqsVw5Le0So6M0Do/9W3ww8o41K7Vg0bgln/bCSunjmpt5rUrtHCAHDF66EIig6GfQqDkt4cQAQpi+xgS0/SUi0uMMMvcHlmSDEG0w3/C016FZjxbzdJlx7wl5dbM9PGKe90pRmTbWyX9kvaa+5vDkjtvGDplW+GANqLijFPcIG5wRMZ9md2KOa7l/kzblcEhllw3ivUVDrF9xv901hjRxDou4uOzYybUiNz5hC+Q0TZZgX3lsYLvOj6gFc5Kp5JVioJ6mta+PuvhmMObQ73tNN82lhvh1rv66sdq3tN4iQW85lDfYxVfsMkyYpzhEj/xy+t7596F9/0v1Zuocl7gv+X9+AO6pZ9i</latexit><latexit sha1_base64="tdLIqvvWZ5dCisSXvHjOp73tm0A=">AAAC9XichVFNSxxBEH1OEr8SzSY55jK4BALBZSYEogFBEiO5CApuFFxZesZ2bHZ2Zuzp1d0s+yP8A54k1xy9Jj8j/hYPed2ZDUQRe+ip6levXld1RUWqShMEvye8Bw8fTU5Nz8w+fjI3/7T27PnXMu/pWDbjPM31biRKmapMNo0yqdwttBTdKJU7UeeTje+cSF2qPNs2g0Lud0WSqUMVC0OoXXvTbyu/lcljv98eqsVw5Le0So6M0Do/9W3ww8o41K7Vg0bgln/bCSunjmpt5rUrtHCAHDF66EIig6GfQqDkt4cQAQpi+xgS0/SUi0uMMMvcHlmSDEG0w3/C016FZjxbzdJlx7wl5dbM9PGKe90pRmTbWyX9kvaa+5vDkjtvGDplW+GANqLijFPcIG5wRMZ9md2KOa7l/kzblcEhllw3ivUVDrF9xv901hjRxDou4uOzYybUiNz5hC+Q0TZZgX3lsYLvOj6gFc5Kp5JVioJ6mta+PuvhmMObQ73tNN82lhvh1rv66sdq3tN4iQW85lDfYxVfsMkyYpzhEj/xy+t7596F9/0v1Zuocl7gv+X9+AO6pZ9i</latexit><latexit sha1_base64="tdLIqvvWZ5dCisSXvHjOp73tm0A=">AAAC9XichVFNSxxBEH1OEr8SzSY55jK4BALBZSYEogFBEiO5CApuFFxZesZ2bHZ2Zuzp1d0s+yP8A54k1xy9Jj8j/hYPed2ZDUQRe+ip6levXld1RUWqShMEvye8Bw8fTU5Nz8w+fjI3/7T27PnXMu/pWDbjPM31biRKmapMNo0yqdwttBTdKJU7UeeTje+cSF2qPNs2g0Lud0WSqUMVC0OoXXvTbyu/lcljv98eqsVw5Le0So6M0Do/9W3ww8o41K7Vg0bgln/bCSunjmpt5rUrtHCAHDF66EIig6GfQqDkt4cQAQpi+xgS0/SUi0uMMMvcHlmSDEG0w3/C016FZjxbzdJlx7wl5dbM9PGKe90pRmTbWyX9kvaa+5vDkjtvGDplW+GANqLijFPcIG5wRMZ9md2KOa7l/kzblcEhllw3ivUVDrF9xv901hjRxDou4uOzYybUiNz5hC+Q0TZZgX3lsYLvOj6gFc5Kp5JVioJ6mta+PuvhmMObQ73tNN82lhvh1rv66sdq3tN4iQW85lDfYxVfsMkyYpzhEj/xy+t7596F9/0v1Zuocl7gv+X9+AO6pZ9i</latexit>

xi = xi�1 !(p : xi := 0

1� p : xi := 1<latexit sha1_base64="iwb+eIGi+9hxPWvDOxQ7Oki74j8=">AAADJXichVFNaxRBEH0Zv5L1a9Wjl8ZF8ZJlRgQ1EAh+4UWI4JrATlh6ZjuTZmd7hp7emLjs//Fv+Ac8iaAXj1717sHX7UTUIKmhp6pfvXpd3ZXVpW5cHH9aik6dPnP23PJK5/yFi5cud69cfdVUM5urQV6Vld3OZKNKbdTAaVeq7doqOc1KtZVNHvn81r6yja7MS3dYq52pLIze1bl0hEbd4cFIi3VxMJrr1WQhUquLPSetrV6LNFOFNvOc6s2iI2j1mrjl+WvrIk7TACWrf4AJoVSZcVsz6vbifhxMHA+SNuihtc2q+xkpxqiQY4YpFAwc4xISDb8hEsSoie1gTswy0iGvsECHtTOyFBmS6IT/grthixruvWYTqnOeUnJZVgrc5HoaFDOy/amKcUP/g+tNwIr/njAPyr7DQ/qMiitB8Tlxhz0yTqqctsyjXk6u9Ldy2MX9cBvN/uqA+Hvmv3UeM2OJTUJG4ElgFtTIwn6fL2DoB+zAv/KRggg3HtPL4FVQMa2ipJ6l96/Pfjjm5N+hHg8Gd/oP+smLu72Nh+28l3EdN3CbQ72HDTzDJtvI8Q5f8Q3fo7fR++hD9PEXNVpqa67hL4u+/AQ6hK33</latexit><latexit sha1_base64="iwb+eIGi+9hxPWvDOxQ7Oki74j8=">AAADJXichVFNaxRBEH0Zv5L1a9Wjl8ZF8ZJlRgQ1EAh+4UWI4JrATlh6ZjuTZmd7hp7emLjs//Fv+Ac8iaAXj1717sHX7UTUIKmhp6pfvXpd3ZXVpW5cHH9aik6dPnP23PJK5/yFi5cud69cfdVUM5urQV6Vld3OZKNKbdTAaVeq7doqOc1KtZVNHvn81r6yja7MS3dYq52pLIze1bl0hEbd4cFIi3VxMJrr1WQhUquLPSetrV6LNFOFNvOc6s2iI2j1mrjl+WvrIk7TACWrf4AJoVSZcVsz6vbifhxMHA+SNuihtc2q+xkpxqiQY4YpFAwc4xISDb8hEsSoie1gTswy0iGvsECHtTOyFBmS6IT/grthixruvWYTqnOeUnJZVgrc5HoaFDOy/amKcUP/g+tNwIr/njAPyr7DQ/qMiitB8Tlxhz0yTqqctsyjXk6u9Ldy2MX9cBvN/uqA+Hvmv3UeM2OJTUJG4ElgFtTIwn6fL2DoB+zAv/KRggg3HtPL4FVQMa2ipJ6l96/Pfjjm5N+hHg8Gd/oP+smLu72Nh+28l3EdN3CbQ72HDTzDJtvI8Q5f8Q3fo7fR++hD9PEXNVpqa67hL4u+/AQ6hK33</latexit><latexit sha1_base64="iwb+eIGi+9hxPWvDOxQ7Oki74j8=">AAADJXichVFNaxRBEH0Zv5L1a9Wjl8ZF8ZJlRgQ1EAh+4UWI4JrATlh6ZjuTZmd7hp7emLjs//Fv+Ac8iaAXj1717sHX7UTUIKmhp6pfvXpd3ZXVpW5cHH9aik6dPnP23PJK5/yFi5cud69cfdVUM5urQV6Vld3OZKNKbdTAaVeq7doqOc1KtZVNHvn81r6yja7MS3dYq52pLIze1bl0hEbd4cFIi3VxMJrr1WQhUquLPSetrV6LNFOFNvOc6s2iI2j1mrjl+WvrIk7TACWrf4AJoVSZcVsz6vbifhxMHA+SNuihtc2q+xkpxqiQY4YpFAwc4xISDb8hEsSoie1gTswy0iGvsECHtTOyFBmS6IT/grthixruvWYTqnOeUnJZVgrc5HoaFDOy/amKcUP/g+tNwIr/njAPyr7DQ/qMiitB8Tlxhz0yTqqctsyjXk6u9Ldy2MX9cBvN/uqA+Hvmv3UeM2OJTUJG4ElgFtTIwn6fL2DoB+zAv/KRggg3HtPL4FVQMa2ipJ6l96/Pfjjm5N+hHg8Gd/oP+smLu72Nh+28l3EdN3CbQ72HDTzDJtvI8Q5f8Q3fo7fR++hD9PEXNVpqa67hL4u+/AQ6hK33</latexit><latexit sha1_base64="iwb+eIGi+9hxPWvDOxQ7Oki74j8=">AAADJXichVFNaxRBEH0Zv5L1a9Wjl8ZF8ZJlRgQ1EAh+4UWI4JrATlh6ZjuTZmd7hp7emLjs//Fv+Ac8iaAXj1717sHX7UTUIKmhp6pfvXpd3ZXVpW5cHH9aik6dPnP23PJK5/yFi5cud69cfdVUM5urQV6Vld3OZKNKbdTAaVeq7doqOc1KtZVNHvn81r6yja7MS3dYq52pLIze1bl0hEbd4cFIi3VxMJrr1WQhUquLPSetrV6LNFOFNvOc6s2iI2j1mrjl+WvrIk7TACWrf4AJoVSZcVsz6vbifhxMHA+SNuihtc2q+xkpxqiQY4YpFAwc4xISDb8hEsSoie1gTswy0iGvsECHtTOyFBmS6IT/grthixruvWYTqnOeUnJZVgrc5HoaFDOy/amKcUP/g+tNwIr/njAPyr7DQ/qMiitB8Tlxhz0yTqqctsyjXk6u9Ldy2MX9cBvN/uqA+Hvmv3UeM2OJTUJG4ElgFtTIwn6fL2DoB+zAv/KRggg3HtPL4FVQMa2ipJ6l96/Pfjjm5N+hHg8Gd/oP+smLu72Nh+28l3EdN3CbQ72HDTzDJtvI8Q5f8Q3fo7fR++hD9PEXNVpqa67hL4u+/AQ6hK33</latexit>

hQF2M BM xi- B7 xi = xi�1<latexit sha1_base64="vWzQF4nKtGodL1Hqlx97ZJAtcow=">AAAC+HichVFNT9tAEH1xCwVKaShHLqtGlXpoIxtVgh6QUEsRF6RUIoBEUGSbTVjFWVv2BkGt/Iv+AU6o1x57bf8E/BYOvF1MJRpVrLWemTczb+cjyhJVGN+/qnlPnk5NP5uZnXs+/2LhZX3x1V6RjvJYtuM0SfODKCxkorRsG2USeZDlMhxGidyPBp+tf/9U5oVK9a45z+TRMOxr1VNxaAh1682OkWem3E0HUgulxVicdZW4A98J1RNja68TLdX7YNytN/ym746YVIJKaaA6rbR+jQ6OkSLGCENIaBjqCUIU/A4RwEdG7AglsZyacn6JMeaYO2KUZERIdMB/n9ZhhWralrNw2TFfSXhzZgq84d1yjBGj7auSekF5w/vNYf3/vlA6ZlvhOWVExlnHuEPc4IQRj2UOq8j7Wh7PtF0Z9LDmulGsL3OI7TP+y7NJT05s4DwCX1xknxyRs085AU3ZZgV2yvcMwnV8TBk6KR2LrhhD8uWUdvqsh2sO/l3qpNJeaX5sBl8/NDY+VfuewTJe4y2XuooNbKPFMmJ8xy/8xh+v9C68S+/HXahXq3KW8OB4P28BP8mgsA==</latexit><latexit sha1_base64="vWzQF4nKtGodL1Hqlx97ZJAtcow=">AAAC+HichVFNT9tAEH1xCwVKaShHLqtGlXpoIxtVgh6QUEsRF6RUIoBEUGSbTVjFWVv2BkGt/Iv+AU6o1x57bf8E/BYOvF1MJRpVrLWemTczb+cjyhJVGN+/qnlPnk5NP5uZnXs+/2LhZX3x1V6RjvJYtuM0SfODKCxkorRsG2USeZDlMhxGidyPBp+tf/9U5oVK9a45z+TRMOxr1VNxaAh1682OkWem3E0HUgulxVicdZW4A98J1RNja68TLdX7YNytN/ym746YVIJKaaA6rbR+jQ6OkSLGCENIaBjqCUIU/A4RwEdG7AglsZyacn6JMeaYO2KUZERIdMB/n9ZhhWralrNw2TFfSXhzZgq84d1yjBGj7auSekF5w/vNYf3/vlA6ZlvhOWVExlnHuEPc4IQRj2UOq8j7Wh7PtF0Z9LDmulGsL3OI7TP+y7NJT05s4DwCX1xknxyRs085AU3ZZgV2yvcMwnV8TBk6KR2LrhhD8uWUdvqsh2sO/l3qpNJeaX5sBl8/NDY+VfuewTJe4y2XuooNbKPFMmJ8xy/8xh+v9C68S+/HXahXq3KW8OB4P28BP8mgsA==</latexit><latexit sha1_base64="vWzQF4nKtGodL1Hqlx97ZJAtcow=">AAAC+HichVFNT9tAEH1xCwVKaShHLqtGlXpoIxtVgh6QUEsRF6RUIoBEUGSbTVjFWVv2BkGt/Iv+AU6o1x57bf8E/BYOvF1MJRpVrLWemTczb+cjyhJVGN+/qnlPnk5NP5uZnXs+/2LhZX3x1V6RjvJYtuM0SfODKCxkorRsG2USeZDlMhxGidyPBp+tf/9U5oVK9a45z+TRMOxr1VNxaAh1682OkWem3E0HUgulxVicdZW4A98J1RNja68TLdX7YNytN/ym746YVIJKaaA6rbR+jQ6OkSLGCENIaBjqCUIU/A4RwEdG7AglsZyacn6JMeaYO2KUZERIdMB/n9ZhhWralrNw2TFfSXhzZgq84d1yjBGj7auSekF5w/vNYf3/vlA6ZlvhOWVExlnHuEPc4IQRj2UOq8j7Wh7PtF0Z9LDmulGsL3OI7TP+y7NJT05s4DwCX1xknxyRs085AU3ZZgV2yvcMwnV8TBk6KR2LrhhD8uWUdvqsh2sO/l3qpNJeaX5sBl8/NDY+VfuewTJe4y2XuooNbKPFMmJ8xy/8xh+v9C68S+/HXahXq3KW8OB4P28BP8mgsA==</latexit><latexit sha1_base64="vWzQF4nKtGodL1Hqlx97ZJAtcow=">AAAC+HichVFNT9tAEH1xCwVKaShHLqtGlXpoIxtVgh6QUEsRF6RUIoBEUGSbTVjFWVv2BkGt/Iv+AU6o1x57bf8E/BYOvF1MJRpVrLWemTczb+cjyhJVGN+/qnlPnk5NP5uZnXs+/2LhZX3x1V6RjvJYtuM0SfODKCxkorRsG2USeZDlMhxGidyPBp+tf/9U5oVK9a45z+TRMOxr1VNxaAh1682OkWem3E0HUgulxVicdZW4A98J1RNja68TLdX7YNytN/ym746YVIJKaaA6rbR+jQ6OkSLGCENIaBjqCUIU/A4RwEdG7AglsZyacn6JMeaYO2KUZERIdMB/n9ZhhWralrNw2TFfSXhzZgq84d1yjBGj7auSekF5w/vNYf3/vlA6ZlvhOWVExlnHuEPc4IQRj2UOq8j7Wh7PtF0Z9LDmulGsL3OI7TP+y7NJT05s4DwCX1xknxyRs085AU3ZZgV2yvcMwnV8TBk6KR2LrhhD8uWUdvqsh2sO/l3qpNJeaX5sBl8/NDY+VfuewTJe4y2XuooNbKPFMmJ8xy/8xh+v9C68S+/HXahXq3KW8OB4P28BP8mgsA==</latexit>


Herman’s randomized self-stabilizing algorithm

!9

p0

p3p2

p4p1

1

0

1

1

0


xi = xi�1 !(p : xi := 0



Legitimate state:exactly 1 token


Herman’s algorithm

!10

p0

p3p2

p4p1

1

0

1

1

0


xi = xi�1 !(p : xi := 0


11 0

10

Coin fliphQF2M BM xi- B7 xi = xi�1<latexit sha1_base64="vWzQF4nKtGodL1Hqlx97ZJAtcow=">AAAC+HichVFNT9tAEH1xCwVKaShHLqtGlXpoIxtVgh6QUEsRF6RUIoBEUGSbTVjFWVv2BkGt/Iv+AU6o1x57bf8E/BYOvF1MJRpVrLWemTczb+cjyhJVGN+/qnlPnk5NP5uZnXs+/2LhZX3x1V6RjvJYtuM0SfODKCxkorRsG2USeZDlMhxGidyPBp+tf/9U5oVK9a45z+TRMOxr1VNxaAh1682OkWem3E0HUgulxVicdZW4A98J1RNja68TLdX7YNytN/ym746YVIJKaaA6rbR+jQ6OkSLGCENIaBjqCUIU/A4RwEdG7AglsZyacn6JMeaYO2KUZERIdMB/n9ZhhWralrNw2TFfSXhzZgq84d1yjBGj7auSekF5w/vNYf3/vlA6ZlvhOWVExlnHuEPc4IQRj2UOq8j7Wh7PtF0Z9LDmulGsL3OI7TP+y7NJT05s4DwCX1xknxyRs085AU3ZZgV2yvcMwnV8TBk6KR2LrhhD8uWUdvqsh2sO/l3qpNJeaX5sBl8/NDY+VfuewTJe4y2XuooNbKPFMmJ8xy/8xh+v9C68S+/HXahXq3KW8OB4P28BP8mgsA==</latexit><latexit sha1_base64="vWzQF4nKtGodL1Hqlx97ZJAtcow=">AAAC+HichVFNT9tAEH1xCwVKaShHLqtGlXpoIxtVgh6QUEsRF6RUIoBEUGSbTVjFWVv2BkGt/Iv+AU6o1x57bf8E/BYOvF1MJRpVrLWemTczb+cjyhJVGN+/qnlPnk5NP5uZnXs+/2LhZX3x1V6RjvJYtuM0SfODKCxkorRsG2USeZDlMhxGidyPBp+tf/9U5oVK9a45z+TRMOxr1VNxaAh1682OkWem3E0HUgulxVicdZW4A98J1RNja68TLdX7YNytN/ym746YVIJKaaA6rbR+jQ6OkSLGCENIaBjqCUIU/A4RwEdG7AglsZyacn6JMeaYO2KUZERIdMB/n9ZhhWralrNw2TFfSXhzZgq84d1yjBGj7auSekF5w/vNYf3/vlA6ZlvhOWVExlnHuEPc4IQRj2UOq8j7Wh7PtF0Z9LDmulGsL3OI7TP+y7NJT05s4DwCX1xknxyRs085AU3ZZgV2yvcMwnV8TBk6KR2LrhhD8uWUdvqsh2sO/l3qpNJeaX5sBl8/NDY+VfuewTJe4y2XuooNbKPFMmJ8xy/8xh+v9C68S+/HXahXq3KW8OB4P28BP8mgsA==</latexit><latexit sha1_base64="vWzQF4nKtGodL1Hqlx97ZJAtcow=">AAAC+HichVFNT9tAEH1xCwVKaShHLqtGlXpoIxtVgh6QUEsRF6RUIoBEUGSbTVjFWVv2BkGt/Iv+AU6o1x57bf8E/BYOvF1MJRpVrLWemTczb+cjyhJVGN+/qnlPnk5NP5uZnXs+/2LhZX3x1V6RjvJYtuM0SfODKCxkorRsG2USeZDlMhxGidyPBp+tf/9U5oVK9a45z+TRMOxr1VNxaAh1682OkWem3E0HUgulxVicdZW4A98J1RNja68TLdX7YNytN/ym746YVIJKaaA6rbR+jQ6OkSLGCENIaBjqCUIU/A4RwEdG7AglsZyacn6JMeaYO2KUZERIdMB/n9ZhhWralrNw2TFfSXhzZgq84d1yjBGj7auSekF5w/vNYf3/vlA6ZlvhOWVExlnHuEPc4IQRj2UOq8j7Wh7PtF0Z9LDmulGsL3OI7TP+y7NJT05s4DwCX1xknxyRs085AU3ZZgV2yvcMwnV8TBk6KR2LrhhD8uWUdvqsh2sO/l3qpNJeaX5sBl8/NDY+VfuewTJe4y2XuooNbKPFMmJ8xy/8xh+v9C68S+/HXahXq3KW8OB4P28BP8mgsA==</latexit><latexit sha1_base64="vWzQF4nKtGodL1Hqlx97ZJAtcow=">AAAC+HichVFNT9tAEH1xCwVKaShHLqtGlXpoIxtVgh6QUEsRF6RUIoBEUGSbTVjFWVv2BkGt/Iv+AU6o1x57bf8E/BYOvF1MJRpVrLWemTczb+cjyhJVGN+/qnlPnk5NP5uZnXs+/2LhZX3x1V6RjvJYtuM0SfODKCxkorRsG2USeZDlMhxGidyPBp+tf/9U5oVK9a45z+TRMOxr1VNxaAh1682OkWem3E0HUgulxVicdZW4A98J1RNja68TLdX7YNytN/ym746YVIJKaaA6rbR+jQ6OkSLGCENIaBjqCUIU/A4RwEdG7AglsZyacn6JMeaYO2KUZERIdMB/n9ZhhWralrNw2TFfSXhzZgq84d1yjBGj7auSekF5w/vNYf3/vlA6ZlvhOWVExlnHuEPc4IQRj2UOq8j7Wh7PtF0Z9LDmulGsL3OI7TP+y7NJT05s4DwCX1xknxyRs085AU3ZZgV2yvcMwnV8TBk6KR2LrhhD8uWUdvqsh2sO/l3qpNJeaX5sBl8/NDY+VfuewTJe4y2XuooNbKPFMmJ8xy/8xh+v9C68S+/HXahXq3KW8OB4P28BP8mgsA==</latexit>


!11

p0

p3p2

p4p1

1

1

0

0

1


xi = xi�1 !(p : xi := 0



Herman’s algorithm


!12

p0

p3p2

p4p1

1

1

0

0

1


xi = xi�1 !(p : xi := 0



⚡

Recovery


!13

p0

p3p2

p4p1

1

1

0

0

0


xi = xi�1 !(p : xi := 0



⚡

Recovery


!14

p0

p3p2

p4p1

1

1

0

0

0


xi = xi�1 !(p : xi := 0



⚡

Recovery

No legitimate state:3 tokens


!15

p0

p3p2

p4p1

1

1

0

0

0


xi = xi�1 !(p : xi := 0



01 1

01

Coin flipCoin flip

Coin flip

Recovery


!16

p0

p3p2

p4p1

0

1

1

1

0


xi = xi�1 !(p : xi := 0



Self-Stabilizing

Recovery


!17

1

1

0

0

0

0

1

1

1

0

0

0

1

1

0

0

1

1

0

1

…

…

Recovery

Question: How fast is the recovery?


Research questions

• How fast do these algorithms converge? • worst-case recovery time • average recovery time

• How does the randomization influence the recovery time?

!18

Fair coin not optimal

use pMCs [Aflaki et al. - 2017]


Other applications

!19

Probability distribution fitting

Motion planning

Software systems

System design

Dynamic fault trees

Parameter synthesis


What is a parametric Markov chain?

A parametric Markov chain is a DTMC over a set of parameters (or variables).

!20

D = (S,Var,P, s◆,AP, L)

Ss◆

AP, L

Var

(finite) set of states

initial stateatomic propositions & labelling

finite set of parameters or variables

transition probabilitiesP : S ⇥ S ! Q(Var)

Rational FunctionsVar ! Rinstantiation:

Whiteboard: Well-defined, Graph-preserving, Simple


What is Parameter Synthesis?

in the context of probabilistic model checking

!21

• parametric MDPs and robust strategies • richer properties • connections to partially observable MDPs (prominent model in AI)

not touched today

• parametric Markov chain ( i.e. a family of induced Markov chains ) • reachability property

Check the property for every induced Markov chain in the family: Learn something about the effect of the parameters


Knuth-Yao Die

!22

s1

s3 s4

s2 s5

s6 s7

p

p p

pp

q q

1�q 1�q

1�p

1�p 1�p 1�p 1�p


Knuth-Yao Die

!23

s1

s3 s4

s2 s5

s6 s7

p

p p

pp

q q

1�q 1�q

1�p

1�p 1�p 1�p 1�p


Knuth-Yao Die

!24

s1

s3 s4

s2 s5

s6 s7

p

pp

q q

1�q 1�q

1�p

1�p 1�p 1�p1�p

p

p


What is the Output of Parameter Synthesis?

So far, three options have been considered in the literature (to the best of our knowledge)

• Option A: A generalisation of the output of non-parametric Markov Chain model checking

• Option B:A concise description of parameter values that yield satisfactory performance

• Option C: One parameter valuation that yields satisfactory performance

!25


Generalised DTMC “Model Checking”

What is the probability that in a given DTMC T is eventually reached?

!26

pMC = set of Markov chains

induced probabilityInstantiation


State Elimination

!27

p

pp

q q

1�q 1�q

1�p

1�p 1�p 1�p1�p

p

p• Reachability in MCs = Linear Equation System states = rows

State Elimination: Solving Linear Equation Systems while exploiting structure.

• Several heuristics - forward/backward/degree-based • SCC-based approaches & efficient data structures

[Jansen et al. - 2014, CAV15]

Analogous to computing regex from NFAs

[Accepted - 2019, CAV17]

• Borrow from Floyd-Warshall and Fraction-Free Gaussian

[Daws - 2004][Hahn et al - 2011]


State Elimination

!28

s1

s3 s4

s2 s5

s6 s7

p

pp

q q

1�q 1�q

1�p

1�p 1�p 1�p1�p

p

p

[Daws - 2004][Hahn et al - 2011]


State Elimination

!29

s5

s6 s7

p

p

q

1�q

1�p

1�p 1�p

s1

s3 s4

s2

p

q

1�q

1�p

p

p

1�p

[Daws - 2004][Hahn et al - 2011]


State Elimination

!30

s1

s3 s4

s2

p

q

1�q

1�p

p

p

1�p

[Daws - 2004][Hahn et al - 2011]

s1

s2

p · (1�p) · 1�q1�pq

(1�p) · 1�q1�pq


State Elimination

!31

s1

s3 s4

s2

p

q

1�q

1�p

p

p

1�p

s1

s4

s2

p

1�q

p

1�p

p · q

(1�p) · q

[Daws - 2004][Hahn et al - 2011]


State Elimination

!32

s1

s3 s4

s2

p

q

1�q

1�p

p

p

1�p

s1

s4

s2

p

1�q

p

1�p

(1�p) · q

p · q

[Daws - 2004][Hahn et al - 2011]


State Elimination

!33

p

q

1�q

1�p

p

p

1�p

s1

s4

s2

p

p

1�p

q·(1�p)1�pq

1�q1�pq

[Daws - 2004][Hahn et al - 2011]

s1

s4

s2

p

1�q

p

1�p

(1�p) · q

p · q


State Elimination

!34

p

q

1�q

1�p

p

p

1�p p

1�q

p

1�p

(1�p) · q

p · q

s1

s4

s2

p

p

1�p

q·(1�p)1�pq

1�q1�pq

[Daws - 2004][Hahn et al - 2011]


State Elimination

!35

p

q

1�q

1�p

p

p

1�p p

1�q

p

1�p

(1�p) · q

p · q

s1

s4

s2

p

p

1�p

1�q1�pq

q·(1�p)1�pq

s1

s2

p

q·(1�p)1�pq

p · 1�q1�pq

(1�p) · 1�q1�pq


State Elimination

!36

p

q

1�q

1�p

p

p

1�p p

1�q

p

1�p

(1�p) · q

p · q

p

p

1�p

1�q1�pq

q·(1�p)1�pq

s1

s2

p

q·(1�p)1�pq

p · 1�q1�pq

(1�p) · 1�q1�pq


State Elimination

!37

p

q

1�q

1�p

p

p

1�p p

1�q

p

1�p

(1�p) · q

p · q

p

p

1�p

1�q1�pq

q·(1�p)1�pq

s1

s2

p

q·(1�p)1�pq

p · 1�q1�pq

(1�p) · 1�q1�pq

s1

s2

p · (1�p) · 1�q1�pq

(1�p) · 1�q1�pq


The size of the solution

Facts

For a pMC with k parameters, n states and polynomial probabilities of degree d.

• The rational function (actually a polynomial) can be exponential in k (even for acyclic pMCs)

• Hence, computation of the function is exponential in the worst case • For any fixed k, the computation can be done in polynomial time in n and d.

!38

[Information & Computation, 2019]


Computing the rational function

Tool support for state elimination

!39

Using Storm


Result of State Elimination

!40

Rational function over the parameters

Numerically instable

State Elimination12

12

12

12

12

12

12

12

12

12

12

12

12

12 p

q

1�q

1�p

p

p

1�p p

1�q

p

1�p

(1�p) · q

p · q

p

p

1�p

1�q1�pq

q·(1�p)1�pq

p

q·(1�p)1�pq

p · 1�q1�pq

(1�p) · 1�q1�pq p · (1�p) · 1�q

1�pq

(1�p) · 1�q1�pq

large

?

Used by many


Result of State Elimination

!41

(100000

* (5960464477539062500000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000*x^31+702373936490740872940087742602805112667874188094069949758963540019627405253125*y+1450904375022708825682321296378347076778416883393982007472009476183433015546875000*y^2+1864755946862212781696097687854559826846553823287794907364816761374121929687500000000*y^3+1668951994385017644663304962887700020242746670158135295164653664125004492187500000000000*y^4+1102865149919950107236938145739490878327656928384325737735665870684589843750000000000000000*y^5+556547137079102685146960572336091343090015799330093919477074765334472656250000000000000000000*y^6+218742892187106712970110443815793230349572908927046406971833843798828125000000000000000000000000*y^7+67657120501106251590042314841381151405530532495603704972860592041015625000000000000000000000000000*y^8+16518818139533290562094250699015259007637423958616171182550292968750000000000000000000000000000000000*y^9+3172295793253285940594791438727346168066208663418201237548828125000000000000000000000000000000000000000*y^10+474016764439910699755280957262762537268094956223410561523437500000000000000000000000000000000000000000000*y^11+54012878922764075188965754667484772073830752262641357421875000000000000000000000000000000000000000000000000*y^12+162426578488654837092788848277278964025878906250000000000000000000000000000000000000000000000000000000000000000000*y^16+9589665193970181581958253602290550036087890625000000000000000000000000000000000000000000000000000000000000000000*y^15+264718553211154172716577556561825608809590996093750000000000000000000000000000000000000000000000000000000000000*y^14+4536039578070738872212092128811920272247180719775390625000000000000000000000000000000000000000000000000000000*y^13+1197686862314302852123159115280362082895137117450174688158218156239594687237500*x+95367431640625000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000*y^15*x^16+5960464477539062500000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000*y^16*x^15+715255737304687500000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000*y^14*x^17+3337860107421875000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000*y^13*x^18+287256240844726562500000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000*y^13*x^17+7503509521484375000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000*y^15*x^15+446975231170654296875000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000*y^16*x^14+58915615081787109375000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000*y^14*x^16+11666933650970458984375000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000*y^13*x^16+276674289703369140625000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000*y^15*x^14+15642804503440856933593750000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000*y^16*x^13+2282697396278381347656250000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000*y^14*x^15+68187713623046875000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000*y^9*x^22+26035308837890625000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000*y^11*x^20+10848045349121093750000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000*y^12*x^19+47731399536132812500000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000*y^10*x^21+6874685287475585937500000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000*y^9*x^21+2432739257812500000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000*y^11*x^19+973612070083618164062500000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000*y^12*x^18+4636150836944580078125000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000*y^10*x^20+330491340312957763671875000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000*y^9*x^20+107887256336212158203125000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000*y^11*x^18+41361572020053863525390625000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000*y^12*x^17+214244310393333435058593750000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000*y^10*x^19+6264176030117511749267578125000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000*y^10*x^18+3019034684533834457397460937500000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000*y^11*x^17+10077168994217181205749511718750000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000*y^9*x^19+218679320692671780347824096679687500000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000*y^9*x^18+60793009248859964457385012553244829177856445312500000000000000000000000000000000000000000000000000000000000000000000000000000000000000*x^22+297097093148446083068847656250000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000*y^13*x^15+6345081593513488769531250000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000*y^15*x^13+338845650976896286010742187500000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000*y^16*x^12+55243594083261489868164062500000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000*y^14*x^14+1105408189623689651489257812500000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000*y^12*x^16+59778028831328625679016113281250000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000*y^11*x^16+129992351966387640714645385742187500000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000*y^10*x^17+3592059357401546746835708618164062500000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000*y^9*x^17+5314641117812264204025268554687500000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000*y^13*x^14+101276044196971893310546875000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000*y^15*x^12+5079412310205996036529541015625000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000*y^16*x^11+935117828937297344207763671875000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000*y^14*x^13+20832672803782986998558044433593750000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000*y^12*x^15+890128854396262941949367523193359375000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000*y^11*x^15+2035648911116343191161155700683593750000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000*y^10*x^16+571901558644897434730104612251580536365509033203125000000000000000000000000000000000000000000000000000000000000000000000000000000000*x^21+6505156213774121289062116393951794624328613281250000000000000000000000000000000000000000000000000000000000000000000000000000000000000*y*x^20+4662278864207081485787459450836753695607185363769531250000000000000000000000000000000000000000000000000000000000000000000000000000*x^20+50740949360382704311506607784522055442333221435546875000000000000000000000000000000000000000000000000000000000000000000000000000000*y*x^19+33135167684433827765543742066794036569982767105102539062500000000000000000000000000000000000000000000000000000000000000000000000*x^19+254988182506988181965992574576107686781883239746093750000000000000000000000000000000000000000000000000000000000000000000000000000000*y^2*x^18+344159703420344416488877511691944861498808860778808593750000000000000000000000000000000000000000000000000000000000000000000000000*y*x^18+206214676427110066935520381227559859435559809207916259765625000000000000000000000000000000000000000000000000000000000000000000*x^18+1646504023832025205043527293258199844966387748718261718750000000000000000000000000000000000000000000000000000000000000000000000000*y^2*x^17+2038299011679168681536786940969947305159554958343505859375000000000000000000000000000000000000000000000000000000000000000000000*y*x^17+1127322211389075632261649358486635636727344074845314025878906250000000000000000000000000000000000000000000000000000000000000*x^17+10570641372121521126599008680635038021300526442527770996093750000000000000000000000000000000000000000000000000000000000000000*y*x^16+5424244866822483211169983239665545598525955378729104995727539062500000000000000000000000000000000000000000000000000000000*x^16+22993645001020890980508212500416188083495861348173260688781738281250000000000000000000000000000000000000000000000000000*x^15+23106452601151809446728665574330661998398492974563961554050901851429382324218750000000000000000*x^6+282220375348493449273670496972815526950749696894880327939987182617187500000000000000000000000000000000000000000000*x^13+814633149719803971693797397545495451586256966581923839750289916992187500000000000000000000000000000000000000000*x^12+2058599763340274458813037963225830507637034015959815951823577880859375000000000000000000000000000000000000000*x^11+4533805972571849662940067537110289096231331477929786871111489105224609375000000000000000000000000000000000*x^10+8649701137732929064620802335522190772707045156810048754059383544921875000000000000000000000000000000000*x^9+14180901742716694228717298441261618573233200286918166438183461530303955078125000000000000000000000000*x^8+19768861305011757896070993030413059018237150485074765068083490613479614257812500000000000000000000*x^7+85869491666048514675621071964575286298115481225557267665863037109375000000000000000000000000000000000000000000000000*x^14+191895690942957145060818410577251915767042894042200326919555664062500000000000000000000000000000000000000000000000000000*y*x^14+48079588734342979484628751087990163633884616566300392150878906250000000000000000000000000000000000000000000000000000000000*y*x^15+45384594749684045248248501666837650848126535875797271728515625000000000000000000000000000000000000000000000000000000000000000*y^2*x^15+9254240254410034438239473752839744703664484977722167968750000000000000000000000000000000000000000000000000000000000000000000000*y^2*x^16+4808497825168630622016252118027737164762735366821289062500000000000000000000000000000000000000000000000000000000000000000000000000*y^3*x^16+46374914847573314725006580352783203125000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000*y^9*x^16+784364818915966487290409399699586237983703613281250000000000000000000000000000000000000000000000000000000000000000000000000000000000*y^3*x^17+67045466910621389508135652542114257812500000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000*y^8*x^17+872076472686334922296215642452239990234375000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000*y^7*x^17+245018943113270535598234591607177663326263427734375000000000000000000000000000000000000000000000000000000000000000000000000000000000000*y^4*x^17+79902743234754692159260734931659212814437866188681696936262094202117187500000000000000000000000*y*x^5+2058388546930028807324019289544624516121047555182549962806701660156250000000000000000000000000000000000000000000000*y*x^12+5506851751618149843363906448107815507953028740648907079851150512695312500000000000000000000000000000000000000000*y*x^11+12807247187088686914338391857783851884492821833877706586489334106445312500000000000000000000000000000000000000*y*x^10+25742607016468278932641491372187893805127162473967283923154634094238281250000000000000000000000000000000000*y*x^9+44371055242652867795503092118448908537712483766161666436504594360351562500000000000000000000000000000000*y*x^8+64906142572960669729859529604595439687379222830032978488770055224609375000000000000000000000000000000*y*x^7+79465409804267522774613831022256502962794062951074915474482420099713134765625000000000000000000000*y*x^6+133601786703964552750515904364324487821025900771270094244217816299047851562500000000000000000000000*y^2*x^5+671683345508612089491617428580030609830506687459852523803710937500000000000000000000000000000000000000000000000000000*y*x^13+126804776643925610425540969385337176654522315969291454715560976464843750000000000000000000000000000000*y^2*x^6+727628730541493693294188380638800119268188448705618381500244140625000000000000000000000000000000000000000000000000000000*y^2*x^13+2375685088897297207735504135658994909337962986691096575260162353515625000000000000000000000000000000000000000000000000*y^2*x^12+6750246046773726005122590874964537730741206539367203780508041381835937500000000000000000000000000000000000000000000*y^2*x^11+16626570682539104226355300337081519429172653691513843926263809204101562500000000000000000000000000000000000000000*y^2*x^10+35303984001273922226098906036792076605763693898989773322803993225097656250000000000000000000000000000000000000*y^2*x^9+64134307895667165393893134183962415029815169386270539663758579254150390625000000000000000000000000000000000*y^2*x^8+98668702060515029959436978960893000212231232499505306616099172836303710937500000000000000000000000000000*y^2*x^7+194433184541764160647176467328217745945953313156771659851074218750000000000000000000000000000000000000000000000000000000000*y^2*x^14+137755828867665398672868456205884754341941356483945271934910764510498046875000000000000000000000000000*y^3*x^5+124508137770209774402304480156271697628959743589635734016490637908935546875000000000000000000000000000000*y^3*x^6+92079775035876162038938923711207896791858960081052671638744561767578125000000000000000000000000000000000000*y^3*x^7+118155113154753037951073599559724714450188514454364776611328125000000000000000000000000000000000000000000000000000000000000000*y^3*x^14+474821985908667380519463648565926836830656141073346138000488281250000000000000000000000000000000000000000000000000000000000*y^3*x^13+1658179463711531203303107461063457870539393370358817815780639648437500000000000000000000000000000000000000000000000000000*y^3*x^12+5021805579608988921634721320547764044694633563987728581428527832031250000000000000000000000000000000000000000000000000*y^3*x^11+13142513821253073560053977677176049710364323388983511804580688476562500000000000000000000000000000000000000000000000*y^3*x^10+29567180009219130466772524064258281855280416359106831868179321289062500000000000000000000000000000000000000000000*y^3*x^9+56764817443468522277548927757493675355395255550291281657042694091796875000000000000000000000000000000000000000*y^3*x^8+25568278459136748691026672317673344608972990751266479492187500000000000000000000000000000000000000000000000000000000000000000000*y^3*x^15+97949509700726451220417437112119972144411628485736585092953435691833496093750000000000000000000000000000*y^4*x^5+84104759384964618425436847926520519892323365049919644184109712600708007812500000000000000000000000000000000*y^4*x^6+58965357466983385751674874801516495945029052128731918453212223052978515625000000000000000000000000000000000000*y^4*x^7+34380605217672423132512557548877464189756113721931108717299461364746093750000000000000000000000000000000000000000*y^4*x^8+9577094991965824130456900712669496408637583255767822265625000000000000000000000000000000000000000000000000000000000000000000000000*y^4*x^15+48007139390742337283679856421835880406647019743919372558593750000000000000000000000000000000000000000000000000000000000000000000*y^4*x^14+208195283151694492398352037928465835238952309139966964721679687500000000000000000000000000000000000000000000000000000000000000*y^4*x^13+781103772141826214088891448797007105477159508373820781707763671875000000000000000000000000000000000000000000000000000000000*y^4*x^12+2531379820890875519753330475778935502016125888340784311294555664062500000000000000000000000000000000000000000000000000000*y^4*x^11+7064344972938063738616352651026386220830567792014794685840606689453125000000000000000000000000000000000000000000000000*y^4*x^10+16894164916210863465722199645920593724976870566930117427968978881835937500000000000000000000000000000000000000000000*y^4*x^9+1650567071812513487149681491416467452275753021240234375000000000000000000000000000000000000000000000000000000000000000000000000000000*y^4*x^16+52797993139591429246447771662180089950561523437500000000000000000000000000000000000000000000000000000000000000000000000000000000000000000*y^5*x^17+50874350082259317132521630282589390005402001387938029913549858093261718750000000000000000000000000000000000*y^5*x^5+41391671138796621842782167022745914837825335015792175171056480407714843750000000000000000000000000000000000000*y^5*x^6+27433131530291664545814933514630022834243814447547507835634231567382812500000000000000000000000000000000000000000*y^5*x^7+15082310508644116242478270794566427300234428055091439522743225097656250000000000000000000000000000000000000000000000*y^5*x^8+2515167399846298188814683755117121760084629058837890625000000000000000000000000000000000000000000000000000000000000000000000000000000*y^5*x^15+13764547501446347387813207753000145221716856956481933593750000000000000000000000000000000000000000000000000000000000000000000000000*y^5*x^14+64783426388405276644376733609521924428394120931625366210937500000000000000000000000000000000000000000000000000000000000000000000*y^5*x^13+262425175109029596062035938105836732422903752143383026123046875000000000000000000000000000000000000000000000000000000000000000*y^5*x^12+914131873590992531892354924267887866575313842632508277893066406250000000000000000000000000000000000000000000000000000000000*y^5*x^11+2731250803890135858352465660594905313514360661178224325180053710937500000000000000000000000000000000000000000000000000000*y^5*x^10+6968516008508047637704263622380971846183737178981750860214233398437500000000000000000000000000000000000000000000000000*y^5*x^9+394286132828674423385187718743018108844757080078125000000000000000000000000000000000000000000000000000000000000000000000000000000000000*y^5*x^16+8040278401656412373832334403631687164306640625000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000*y^6*x^17+19943372879042413328808957346643205302129483685088707825488433837890625000000000000000000000000000000000000000*y^6*x^5+15330655154855127952037010177735378916559986681523496696178436279296875000000000000000000000000000000000000000000*y^6*x^6+9575467310380560461038235932841538830811168249353755265665054321289062500000000000000000000000000000000000000000000*y^6*x^7+4947227579330178774627876330594971633814946460546321389675140380859375000000000000000000000000000000000000000000000000*y^6*x^8+475955313625551990713500635367065111398696899414062500000000000000000000000000000000000000000000000000000000000000000000000000000000000*y^6*x^15+2865172578258321272505971695755495395543575286865234375000000000000000000000000000000000000000000000000000000000000000000000000000000*y^6*x^14+14730331002077230084269719730305324481707453727722167968750000000000000000000000000000000000000000000000000000000000000000000000000*y^6*x^13+64793171143369703462501570416749855018602477788925170898437500000000000000000000000000000000000000000000000000000000000000000000*y^6*x^12+243823536373380887438033400195261325392206592080593109130859375000000000000000000000000000000000000000000000000000000000000000*y^6*x^11+783471320564821753791528646919824033895224420338797569274902343750000000000000000000000000000000000000000000000000000000000*y^6*x^10+2141313370168082319413239834776211777327215707213229656219482421875000000000000000000000000000000000000000000000000000000*y^6*x^9+67269444372328165993956856520542669296264648437500000000000000000000000000000000000000000000000000000000000000000000000000000000000000000*y^6*x^16+6011188285900138568540988008845032193879154505671110505481719970703125000000000000000000000000000000000000000000*y^7*x^5+4352055277821408266350032449937609680084237927460147336959838867187500000000000000000000000000000000000000000000000*y^7*x^6+2552921595538700394659546119809692289955235357219398465156555175781250000000000000000000000000000000000000000000000000*y^7*x^7+1234864362141330462313321780327800569314741032748962640762329101562500000000000000000000000000000000000000000000000000000*y^7*x^8+65682066751565277685527965521548771858215332031250000000000000000000000000000000000000000000000000000000000000000000000000000000000000000*y^7*x^15+438816052060388429713089056589054858922958374023437500000000000000000000000000000000000000000000000000000000000000000000000000000000000*y^7*x^14+2483101557927140562065415139135833340871334075927734375000000000000000000000000000000000000000000000000000000000000000000000000000000*y^7*x^13+11938057601694546962729174247927094720802378654479980468750000000000000000000000000000000000000000000000000000000000000000000000000*y^7*x^12+48811195056106558254705917613744825298478397130966186523437500000000000000000000000000000000000000000000000000000000000000000000*y^7*x^11+169541195131718106365592699742533555242184653632640838623046875000000000000000000000000000000000000000000000000000000000000000*y^7*x^10+498646794609674868181866148723066432467924959318804740905761718750000000000000000000000000000000000000000000000000000000000*y^7*x^9+8281152270798709796682101071500778198242187500000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000*y^7*x^16+1405807780118441938403318056869113802397723036773709760570526123046875000000000000000000000000000000000000000000000*y^8*x^5+955230576785575447799622728459628678333599851781182374954223632812500000000000000000000000000000000000000000000000000*y^8*x^6+524245819475872935581307877220856361664606241361436486244201660156250000000000000000000000000000000000000000000000000000*y^8*x^7+236415397172860121768182823370287286871083155244976282119750976562500000000000000000000000000000000000000000000000000000000*y^8*x^8+6616353691436821717600317271227240562438964843750000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000*y^8*x^15+49584638268632137199964022241948491334915161132812500000000000000000000000000000000000000000000000000000000000000000000000000000000000000*y^8*x^14+311600853195888010207279323019575394690036773681640625000000000000000000000000000000000000000000000000000000000000000000000000000000000*y^8*x^13+1649982082680167648673515868055409748612046241760253906250000000000000000000000000000000000000000000000000000000000000000000000000000*y^8*x^12+7378714448978601427582113276029678290670496225357055664062500000000000000000000000000000000000000000000000000000000000000000000000*y^8*x^11+27865745000886959424903831831051469039215506136417388916015625000000000000000000000000000000000000000000000000000000000000000000*y^8*x^10+88652819259316089037073784425003470720971039376854896545410156250000000000000000000000000000000000000000000000000000000000000*y^8*x^9+734500767754892340256013862848281860351562500000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000*y^8*x^16+70908645645691418683528900146484375000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000*y^13*x^13+1192685416612513446807861328125000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000*y^15*x^11+55799807113621965050697326660156250000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000*y^16*x^10+11746794992985682921409606933593750000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000*y^14*x^12+294119527343229083243608474731445312500000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000*y^12*x^14+10341142671565822676132130622863769531250000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000*y^11*x^14+24968203908745918733236527442932128906250000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000*y^10*x^15+482288342379842525984776678323745727539062500000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000*y^9*x^15+255506926860090431296529811252808622124873537095457801818847656250000000000000000000000000000000000000000000000000000*y^9*x^5+162306917656670918803432089998552736730857371562538146972656250000000000000000000000000000000000000000000000000000000000*y^9*x^6+28979199409970078950246592945617985725402832031250000000000000000000000000000000000000000000000000000000000000000000000000000000000000000*y^9*x^13+170541780619083049134351197739354198694229125976562500000000000000000000000000000000000000000000000000000000000000000000000000000000000*y^9*x^12+840622337037292964179798834143789765667915344238281250000000000000000000000000000000000000000000000000000000000000000000000000000000*y^9*x^11+3474849822571031436193508445452583049099969863891601562500000000000000000000000000000000000000000000000000000000000000000000000000*y^9*x^10+12028820873410360805514747068046079760173973798751831054687500000000000000000000000000000000000000000000000000000000000000000000*y^9*x^9+34724998656879561278532662617430350265287313916683197021484375000000000000000000000000000000000000000000000000000000000000000*y^9*x^8+82983293937163916669239955430897061442775017621183395385742187500000000000000000000000000000000000000000000000000000000000*y^9*x^7+4107916386738483861709129973857402801513671875000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000*y^9*x^14+35900687560019528551298826473918151500435313739631652832031250000000000000000000000000000000000000000000000000000000000*y^10*x^5+21227038278228296592836284776426627512152493919754028320312500000000000000000000000000000000000000000000000000000000000000*y^10*x^6+1971785072926736968500440139377117156982421875000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000*y^10*x^13+13037078500323928172151519947609639167785644531250000000000000000000000000000000000000000000000000000000000000000000000000000000000000000*y^10*x^12+71479494758942867626605903252792113065719604492187500000000000000000000000000000000000000000000000000000000000000000000000000000000000*y^10*x^11+325953564190573249158932069395673192083835601806640625000000000000000000000000000000000000000000000000000000000000000000000000000000*y^10*x^10+1236120252388399104820026027837091217595195770263671875000000000000000000000000000000000000000000000000000000000000000000000000000*y^10*x^9+3886147826066156511700042301173414826486867666244506835937500000000000000000000000000000000000000000000000000000000000000000000*y^10*x^8+10061870886295559704261481181095914378238383526802062988281250000000000000000000000000000000000000000000000000000000000000000*y^10*x^7+245725756724279105916196462392807006835937500000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000*y^10*x^14+3850019782983808235711177482807167011219822411727905273437500000000000000000000000000000000000000000000000000000000000000*y^11*x^5+722435595851420564438448645861148834228515625000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000*y^11*x^12+4454416836428993866640264569952750205993652343750000000000000000000000000000000000000000000000000000000000000000000000000000000000000000*y^11*x^11+22615975999243537948559930487286119222640991210937500000000000000000000000000000000000000000000000000000000000000000000000000000000000*y^11*x^10+94707045725196342033039966959729478514194488525390625000000000000000000000000000000000000000000000000000000000000000000000000000000*y^11*x^9+326500730909408747284712396684391066306948661804199218750000000000000000000000000000000000000000000000000000000000000000000000000*y^11*x^8+921530488210140917522822001201004440672276973724365234375000000000000000000000000000000000000000000000000000000000000000000000*y^11*x^7+2108426781387263768352630493637386012374082298278808593750000000000000000000000000000000000000000000000000000000000000000000*y^11*x^6+95967979355255888602478657960891723632812500000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000*y^11*x^13+308118492383997293871293831083556127253985652923583984375000000000000000000000000000000000000000000000000000000000000000000*y^12*x^5+731140518928607392125773429870605468750000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000*y^13*x^12+28110228734570530471623932480812072753906250000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000*y^12*x^12+5956011789461831081228929758071899414062500000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000*y^13*x^11+858466507424990087248485088348388671875000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000*y^14*x^10+38851997920297529494302445461750030517578125000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000*y^13*x^10+10717412922179424173545837402343750000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000*y^15*x^10+463937019386948959809541702270507812500000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000*y^16*x^9+74941344780044301466756820678710937500000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000*y^15*x^9+113370463586834726901769638061523437500000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000*y^14*x^11+2971906447214927179975092411041259765625000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000*y^16*x^8+412007459374282785891305112838745117187500000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000*y^15*x^8+5162381850940973164221820554733276367187500000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000*y^14*x^9+204425392092458555317682774888348579406738281250000000000000000000000000000000000000000000000000000000000000000000000000000000000000000*y^13*x^9+197550154037969817449444505611658096313476562500000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000*y^12*x^11+1129195616960682347199521095417988300323486328125000000000000000000000000000000000000000000000000000000000000000000000000000000000000000*y^12*x^10+5270709271402146391391294443267263054847717285156250000000000000000000000000000000000000000000000000000000000000000000000000000000000*y^12*x^9+24789551887290065779286412694835662841796875000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000*y^14*x^8+869521078284347904133035246312595605850219726562500000000000000000000000000000000000000000000000000000000000000000000000000000000000*y^13*x^8+20087220603742421427116644847348386377096176147460937500000000000000000000000000000000000000000000000000000000000000000000000000000*y^12*x^8+62241253299926428016585932715075110253405570983886718750000000000000000000000000000000000000000000000000000000000000000000000000*y^12*x^7+8185829103885753360953268229684206233596801757812500000000000000000000000000000000000000000000000000000000000000000000000000000*y^13*x^6+155411880811466846588579112327581539171319961547851562500000000000000000000000000000000000000000000000000000000000000000000000*y^12*x^6+2982319550235374579157616455643413224220275878906250000000000000000000000000000000000000000000000000000000000000000000000000000000*y^13*x^7+1786423000301954182133480785560607910156250000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000*y^15*x^7+57097992576601338862419163227081298828125000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000*y^16*x^6+6087235396142827412597484237487792968750000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000*y^15*x^6+169760619651267772885016052535057067871093750000000000000000000000000000000000000000000000000000000000000000000000000000000000000*y^16*x^5+16126309650557470487178846840023803710937500000000000000000000000000000000000000000000000000000000000000000000000000000000000000*y^15*x^5+95038208833468030197324098091958999633789062500000000000000000000000000000000000000000000000000000000000000000000000000000000000000*y^14*x^7+289194277983191713677191677033813095092773437500000000000000000000000000000000000000000000000000000000000000000000000000000000000*y^14*x^6+689802147069623752019023122667773573303222656250000000000000000000000000000000000000000000000000000000000000000000000000000000*y^14*x^5+17734708808973298710295640003493808144741058349609375000000000000000000000000000000000000000000000000000000000000000000000000*y^13*x^5+14784131420669592824098478555679321289062500000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000*y^16*x^7+3225394262741212993549406528472900390625000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000*y^12*x^13+110592725904786272851364667086456329822540283203125000000000000000000000000000000000000000000000000000000000000000000000000000000000000*y^3*x^18+31178686783658281254619218155774044990539550781250000000000000000000000000000000000000000000000000000000000000000000000000000000000000000*y^4*x^18+4947016877281525708043575286865234375000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000*y^8*x^18+75777632192249841103258371353149414062500000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000*y^7*x^18+805504483574650743155251671791076660156250000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000*y^6*x^18+6000015634537550225473873924362659454345703125000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000*y^5*x^18+34241008446476757783448258353397873401641845703125000000000000000000000000000000000000000000000000000000000000000000000000000000000000*y^2*x^19+721034974690949901153326456071758270263671875000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000*y*x^21+68563252099540461487267554004192352294921875000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000*y*x^22+3965164131391507143106579120227408409118652343750000000000000000000000000000000000000000000000000000000000000000000000000000000000000000*y^2*x^20+13408924405083938583057513514886283874511718750000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000*y^3*x^19+3377610364907914784048630755121707916259765625000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000*y^4*x^19+76711177825927734375000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000*y^8*x^23+8017085194587707519531250000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000*y^8*x^22+12707371053225409984588623046875000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000*y^8*x^20+287783353344089934110641479492187500000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000*y^8*x^19+5339194816227069378561973571777343750000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000*y^7*x^19+66795066052877685469540119171142578125000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000*y^6*x^19+573313423433073478775714479207992553710937500000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000*y^5*x^19+400326728721857070922851562500000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000*y^8*x^21+1387974536054033303673559725911617279052734375000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000*y^3*x^20+68187713623046875000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000*y^7*x^24+7377910614013671875000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000*y^7*x^23+12607045777819347381591796875000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000*y^7*x^21+297418227208933067321777343750000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000*y^7*x^20+4503849521784642431674003601074218750000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000*y^6*x^20+45470629447284533902035212516784667968750000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000*y^5*x^20+308524377532064845818608916640281677246093750000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000*y^4*x^20+382127222881317138671875000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000*y^7*x^22+393011088801602106949167977156639099121093750000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000*y^2*x^21+26035308837890625000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000*y^5*x^26+47731399536132812500000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000*y^6*x^25+3009160995483398437500000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000*y^5*x^25+5340666294097900390625000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000*y^6*x^24+167033812732696533203125000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000*y^5*x^24+8863952653885747504585671424865722656250000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000*y^3*x^22+33005561334220270817461417913436889648437500000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000*y^2*x^22+5927300540040373802185058593750000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000*y^5*x^23+9810773399543237686157226562500000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000*y^6*x^22+150998672265779428720474243164062500000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000*y^5*x^22+240698356742239551544189453125000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000*y^6*x^21+2939888492529790335862636566162109375000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000*y^5*x^21+1456500201571123118876218795776367187500000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000*y^4*x^22+23451511192943723830720126628875732421875000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000*y^4*x^21+121451565189936748742560593843460083007812500000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000*y^3*x^21+286534545989036560058593750000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000*y^6*x^23+5555741709590614607193674913048744201660156250000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000*x^23+95367431640625000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000*y*x^30+798881053924560546875000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000*x^30+12430191040039062500000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000*y*x^29+90587139129638671875000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000*y^2*x^28+782200412750244140625000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000*y*x^28+3337860107421875000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000*y^3*x^28+10848045349121093750000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000*y^4*x^27+410423278808593750000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000*y^3*x^27+715255737304687500000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000*y^2*x^29+1293846368789672851562500000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000*y^4*x^26+24305086727142333984375000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000*y^3*x^26+5532508187294006347656250000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000*y^2*x^27+31646798063206672668457031250000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000*y*x^27+51751813292503356933593750000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000*x^29+2158023881286382675170898437500000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000*x^28+65087762878424823284149169921875000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000*x^27+216968289755439758300781250000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000*y^2*x^26+924905691554619073867797851562500000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000*y*x^26+1512579509390543066859245300292968750000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000*x^26+28173055976082432635706663131713867187500000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000*x^25+374305482429900182069921493530273437500000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000*y*x^24+431942757997155853650200068950653076171875000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000*x^24+20798847150531265501976013183593750000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000*y*x^25+922968854705190658569335937500000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000*y^3*x^25+2726170398240280151367187500000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000*y^4*x^24+25245891877856787681579589843750000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000*y^3*x^24+72010921616599508404731750488281250000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000*y^4*x^23+529687979059695770251750946044921875000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000*y^3*x^23+6138022252907994985580444335937500000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000*y^2*x^25+133409464420846990141868591308593750000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000*y^2*x^24+2316785442327712265708088874816894531250000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000*y^2*x^23+5535820647861757518793185949325561523437500000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000*y*x^23+74220770018100738525390625000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000*y^4*x^25+22216855717799718657878177855346282990737231468180672325152136075953309326171875000000000000*x^5+10143760622958795283251174272834031222961905328211327275265648696174398842773437500000*x^3+17108861769411732152099358378553115149213862107690441163554314365394520019531250000000000*x^4+17725006203208130467619466143774248213298307071052582152499427974076633792968750000000*y*x^2+64251398048687113087434121819893753025695666793191659168571149547405249023437500000000000000*y*x^4+39722815325743092303555600787785420202076727048649620539565981706761677197265625000000000*y*x^3+33780561302583526513659623196224067419911220122034151639888406576618945751953125000000000*y^2*x^2+72577271666491952237494241492312913904998079501547778287321419105228436279296875000000000000*y^2*x^3+112387014590558551943486520444808722394579435462278010033282262099825500488281250000000000000000*y^2*x^4+39926691396401745224476043600416150601779927103145759622835489872288286132812500000000000000*y^3*x^2+82093444720391743777785592781894670766149179153680100435148575961637573242187500000000000000000*y^3*x^3+121471855927145956891673429284227939178571192750043859333049912544854736328125000000000000000000000*y^3*x^4+32746293550792920744656392475617161377570838257217043459530533697137329101562500000000000000000*y^4*x^2+64309485142658212261923079360994235598659313544407504924140952985659790039062500000000000000000000*y^4*x^3+90738864434428871379649058820576886075553196564137733435325841812591552734375000000000000000000000000*y^4*x^4+19752980375152338115775202466068671692473487717545346608610410453515625000000000000000000000000000*y^5*x^2+36973360508975595305970877168031130509954294247729183005202590519714355468750000000000000000000000000*y^5*x^3+49633131664198187654624119663402576882758346460638795057276235778808593750000000000000000000000000000000*y^5*x^4+9060640113416542201754759200408102686704034359983993557473464483337402343750000000000000000000000000*y^6*x^2+16126734148084426261913904725867418543138347743603915271347324653625488281250000000000000000000000000000*y^6*x^3+20545293502827494686710612122731987902949440497260563495530311203002929687500000000000000000000000000000000*y^6*x^4+3221943184373780786702120184056855523280266129975120476625443756103515625000000000000000000000000000000*y^7*x^2+54391059407583406776111533492776316825892185864627838519262275695800781250000000000000000

41 States - 138 Transitions - 2 Parameters

The numerator has 408 terms, The denominator is the product of 48 linear polynomials

5 seconds



So far, three options have been considered in the literature




!42


Parameter Space Partitioning

!43


SMT-Encoding

Encoding transition system, satisfiability (region)

!44


Checking Regions

!45

State Elimination12

12

12

12

12

12

12

12

12

12

12

12

12

12

p

q

1�q

1�p

p

p

1�p p

1�q

p

1�p

(1�p) · q

p · q

p

p

1�p

1�q1�pq

q·(1�p)1�pq

p

q·(1�p)1�pq

p · 1�q1�pq

(1�p) · 1�q1�pq p · (1�p) · 1�q

1�pq

(1�p) · 1�q1�pq

(100000 * (5960464477539062500000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000*x^31+702373936490740872940087742602805112667874188094069949758963540019627405253125*y+1450904375022708825682321296378347076778416883393982007472009476183433015546875000*y^2+1864755946862212781696097687854559826846553823287794907364816761374121929687500000000*y^3+1668951994385017644663304962887700020242746670158135295164653664125004492187500000000000*y^4+1102865149919950107236938145739490878327656928384325737735665870684589843750000000000000000*y^5+556547137079102685146960572336091343090015799330093919477074765334472656250000000000000000000*y^6+218742892187106712970110443815793230349572908927046406971833843798828125000000000000000000000000*y^7+67657120501106251590042314841381151405530532495603704972860592041015625000000000000000000000000000*y^8+16518818139533290562094250699015259007637423958616171182550292968750000000000000000000000000000000000*y^9+3172295793253285940594791438727346168066208663418201237548828125000000000000000000000000000000000000000*y^10+474016764439910699755280957262762537268094956223410561523437500000000000000000000000000000000000000000000*y^11+54012878922764075188965754667484772073830752262641357421875000000000000000000000000000000000000000000000000*y^12+162426578488654837092788848277278964025878906250000000000000000000000000000000000000000000000000000000000000000000*y^16+9589665193970181581958253602290550036087890625000000000000000000000000000000000000000000000000000000000000000000*y^15+264718553211154172716577556561825608809590996093750000000000000000000000000000000000000000000000000000000000000*y^14+4536039578070738872212092128811920272247180719775390625000000000000000000000000000000000000000000000000000000*y^13+1197686862314302852123159115280362082895137117450174688158218156239594687237500*x+95367431640625000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000*y^15*x^16+5960464477539062500000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000*y^16*x^15+715255737304687500000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000*y^14*x^17+3337860107421875000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000*y^13*x^18+287256240844726562500000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000*y^13*x^17+7503509521484375000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000*y^15*x^15+446975231170654296875000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000*y^16*x^14+58915615081787109375000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000*y^14*x^16+11666933650970458984375000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000*y^13*x^16+276674289703369140625000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000*y^15*x^14+15642804503440856933593750000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000*y^16*x^13+2282697396278381347656250000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000*y^14*x^15+68187713623046875000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000*y^9*x^22+26035308837890625000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000*y^11*x^20+10848045349121093750000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000*y^12*x^19+47731399536132812500000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000*y^10*x^21+6874685287475585937500000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000*y^9*x^21+2432739257812500000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000*y^11*x^19+973612070083618164062500000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000*y^12*x^18+4636150836944580078125000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000*y^10*x^20+330491340312957763671875000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000*y^9*x^20+107887256336212158203125000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000*y^11*x^18+41361572020053863525390625000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000*y^12*x^17+214244310393333435058593750000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000*y^10*x^19+6264176030117511749267578125000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000*y^10*x^18+3019034684533834457397460937500000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000*y^11*x^17+10077168994217181205749511718750000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000*y^9*x^19+218679320692671780347824096679687500000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000*y^9*x^18+60793009248859964457385012553244829177856445312500000000000000000000000000000000000000000000000000000000000000000000000000000000000000*x^22+297097093148446083068847656250000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000*y^13*x^15+6345081593513488769531250000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000*y^15*x^13+338845650976896286010742187500000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000*y^16*x^12+55243594083261489868164062500000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000*y^14*x^14+1105408189623689651489257812500000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000*y^12*x^16+59778028831328625679016113281250000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000*y^11*x^16+129992351966387640714645385742187500000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000*y^10*x^17+3592059357401546746835708618164062500000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000*y^9*x^17+5314641117812264204025268554687500000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000*y^13*x^14+101276044196971893310546875000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000*y^15*x^12+5079412310205996036529541015625000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000*y^16*x^11+935117828937297344207763671875000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000*y^14*x^13+20832672803782986998558044433593750000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000*y^12*x^15+890128854396262941949367523193359375000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000*y^11*x^15+2035648911116343191161155700683593750000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000*y^10*x^16+571901558644897434730104612251580536365509033203125000000000000000000000000000000000000000000000000000000000000000000000000000000000*x^21+6505156213774121289062116393951794624328613281250000000000000000000000000000000000000000000000000000000000000000000000000000000000000*y*x^20+4662278864207081485787459450836753695607185363769531250000000000000000000000000000000000000000000000000000000000000000000000000000*x^20+50740949360382704311506607784522055442333221435546875000000000000000000000000000000000000000000000000000000000000000000000000000000*y*x^19+33135167684433827765543742066794036569982767105102539062500000000000000000000000000000000000000000000000000000000000000000000000*x^19+254988182506988181965992574576107686781883239746093750000000000000000000000000000000000000000000000000000000000000000000000000000000*y^2*x^18+344159703420344416488877511691944861498808860778808593750000000000000000000000000000000000000000000000000000000000000000000000000*y*x^18+206214676427110066935520381227559859435559809207916259765625000000000000000000000000000000000000000000000000000000000000000000*x^18+1646504023832025205043527293258199844966387748718261718750000000000000000000000000000000000000000000000000000000000000000000000000*y^2*x^17+2038299011679168681536786940969947305159554958343505859375000000000000000000000000000000000000000000000000000000000000000000000*y*x^17+1127322211389075632261649358486635636727344074845314025878906250000000000000000000000000000000000000000000000000000000000000*x^17+10570641372121521126599008680635038021300526442527770996093750000000000000000000000000000000000000000000000000000000000000000*y*x^16+5424244866822483211169983239665545598525955378729104995727539062500000000000000000000000000000000000000000000000000000000*x^16+22993645001020890980508212500416188083495861348173260688781738281250000000000000000000000000000000000000000000000000000*x^15+23106452601151809446728665574330661998398492974563961554050901851429382324218750000000000000000*x^6+282220375348493449273670496972815526950749696894880327939987182617187500000000000000000000000000000000000000000000*x^13+814633149719803971693797397545495451586256966581923839750289916992187500000000000000000000000000000000000000000*x^12+2058599763340274458813037963225830507637034015959815951823577880859375000000000000000000000000000000000000000*x^11+4533805972571849662940067537110289096231331477929786871111489105224609375000000000000000000000000000000000*x^10+8649701137732929064620802335522190772707045156810048754059383544921875000000000000000000000000000000000*x^9+14180901742716694228717298441261618573233200286918166438183461530303955078125000000000000000000000000*x^8+19768861305011757896070993030413059018237150485074765068083490613479614257812500000000000000000000*x^7+85869491666048514675621071964575286298115481225557267665863037109375000000000000000000000000000000000000000000000000*x^14+191895690942957145060818410577251915767042894042200326919555664062500000000000000000000000000000000000000000000000000000*y*x^14+48079588734342979484628751087990163633884616566300392150878906250000000000000000000000000000000000000000000000000000000000*y*x^15+45384594749684045248248501666837650848126535875797271728515625000000000000000000000000000000000000000000000000000000000000000*y^2*x^15+9254240254410034438239473752839744703664484977722167968750000000000000000000000000000000000000000000000000000000000000000000000*y^2*x^16+4808497825168630622016252118027737164762735366821289062500000000000000000000000000000000000000000000000000000000000000000000000000*y^3*x^16+46374914847573314725006580352783203125000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000*y^9*x^16+784364818915966487290409399699586237983703613281250000000000000000000000000000000000000000000000000000000000000000000000000000000000*y^3*x^17+67045466910621389508135652542114257812500000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000*y^8*x^17+872076472686334922296215642452239990234375000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000*y^7*x^17+245018943113270535598234591607177663326263427734375000000000000000000000000000000000000000000000000000000000000000000000000000000000000*y^4*x^17+79902743234754692159260734931659212814437866188681696936262094202117187500000000000000000000000*y*x^5+2058388546930028807324019289544624516121047555182549962806701660156250000000000000000000000000000000000000000000000*y*x^12+5506851751618149843363906448107815507953028740648907079851150512695312500000000000000000000000000000000000000000*y*x^11+12807247187088686914338391857783851884492821833877706586489334106445312500000000000000000000000000000000000000*y*x^10+25742607016468278932641491372187893805127162473967283923154634094238281250000000000000000000000000000000000*y*x^9+44371055242652867795503092118448908537712483766161666436504594360351562500000000000000000000000000000000*y*x^8+64906142572960669729859529604595439687379222830032978488770055224609375000000000000000000000000000000*y*x^7+79465409804267522774613831022256502962794062951074915474482420099713134765625000000000000000000000*y*x^6+133601786703964552750515904364324487821025900771270094244217816299047851562500000000000000000000000*y^2*x^5+671683345508612089491617428580030609830506687459852523803710937500000000000000000000000000000000000000000000000000000*y*x^13+126804776643925610425540969385337176654522315969291454715560976464843750000000000000000000000000000000*y^2*x^6+727628730541493693294188380638800119268188448705618381500244140625000000000000000000000000000000000000000000000000000000*y^2*x^13+2375685088897297207735504135658994909337962986691096575260162353515625000000000000000000000000000000000000000000000000*y^2*x^12+6750246046773726005122590874964537730741206539367203780508041381835937500000000000000000000000000000000000000000000*y^2*x^11+16626570682539104226355300337081519429172653691513843926263809204101562500000000000000000000000000000000000000000*y^2*x^10+35303984001273922226098906036792076605763693898989773322803993225097656250000000000000000000000000000000000000*y^2*x^9+64134307895667165393893134183962415029815169386270539663758579254150390625000000000000000000000000000000000*y^2*x^8+98668702060515029959436978960893000212231232499505306616099172836303710937500000000000000000000000000000*y^2*x^7+194433184541764160647176467328217745945953313156771659851074218750000000000000000000000000000000000000000000000000000000000*y^2*x^14+137755828867665398672868456205884754341941356483945271934910764510498046875000000000000000000000000000*y^3*x^5+124508137770209774402304480156271697628959743589635734016490637908935546875000000000000000000000000000000*y^3*x^6+92079775035876162038938923711207896791858960081052671638744561767578125000000000000000000000000000000000000*y^3*x^7+118155113154753037951073599559724714450188514454364776611328125000000000000000000000000000000000000000000000000000000000000000*y^3*x^14+474821985908667380519463648565926836830656141073346138000488281250000000000000000000000000000000000000000000000000000000000*y^3*x^13+1658179463711531203303107461063457870539393370358817815780639648437500000000000000000000000000000000000000000000000000000*y^3*x^12+5021805579608988921634721320547764044694633563987728581428527832031250000000000000000000000000000000000000000000000000*y^3*x^11+13142513821253073560053977677176049710364323388983511804580688476562500000000000000000000000000000000000000000000000*y^3*x^10+29567180009219130466772524064258281855280416359106831868179321289062500000000000000000000000000000000000000000000*y^3*x^9+56764817443468522277548927757493675355395255550291281657042694091796875000000000000000000000000000000000000000*y^3*x^8+25568278459136748691026672317673344608972990751266479492187500000000000000000000000000000000000000000000000000000000000000000000*y^3*x^15+97949509700726451220417437112119972144411628485736585092953435691833496093750000000000000000000000000000*y^4*x^5+84104759384964618425436847926520519892323365049919644184109712600708007812500000000000000000000000000000000*y^4*x^6+58965357466983385751674874801516495945029052128731918453212223052978515625000000000000000000000000000000000000*y^4*x^7+34380605217672423132512557548877464189756113721931108717299461364746093750000000000000000000000000000000000000000*y^4*x^8+9577094991965824130456900712669496408637583255767822265625000000000000000000000000000000000000000000000000000000000000000000000000*y^4*x^15+48007139390742337283679856421835880406647019743919372558593750000000000000000000000000000000000000000000000000000000000000000000*y^4*x^14+208195283151694492398352037928465835238952309139966964721679687500000000000000000000000000000000000000000000000000000000000000*y^4*x^13+781103772141826214088891448797007105477159508373820781707763671875000000000000000000000000000000000000000000000000000000000*y^4*x^12+2531379820890875519753330475778935502016125888340784311294555664062500000000000000000000000000000000000000000000000000000*y^4*x^11+7064344972938063738616352651026386220830567792014794685840606689453125000000000000000000000000000000000000000000000000*y^4*x^10+16894164916210863465722199645920593724976870566930117427968978881835937500000000000000000000000000000000000000000000*y^4*x^9+1650567071812513487149681491416467452275753021240234375000000000000000000000000000000000000000000000000000000000000000000000000000000*y^4*x^16+52797993139591429246447771662180089950561523437500000000000000000000000000000000000000000000000000000000000000000000000000000000000000000*y^5*x^17+50874350082259317132521630282589390005402001387938029913549858093261718750000000000000000000000000000000000*y^5*x^5+41391671138796621842782167022745914837825335015792175171056480407714843750000000000000000000000000000000000000*y^5*x^6+27433131530291664545814933514630022834243814447547507835634231567382812500000000000000000000000000000000000000000*y^5*x^7+15082310508644116242478270794566427300234428055091439522743225097656250000000000000000000000000000000000000000000000*y^5*x^8+2515167399846298188814683755117121760084629058837890625000000000000000000000000000000000000000000000000000000000000000000000000000000*y^5*x^15+13764547501446347387813207753000145221716856956481933593750000000000000000000000000000000000000000000000000000000000000000000000000*y^5*x^14+64783426388405276644376733609521924428394120931625366210937500000000000000000000000000000000000000000000000000000000000000000000*y^5*x^13+262425175109029596062035938105836732422903752143383026123046875000000000000000000000000000000000000000000000000000000000000000*y^5*x^12+914131873590992531892354924267887866575313842632508277893066406250000000000000000000000000000000000000000000000000000000000*y^5*x^11+2731250803890135858352465660594905313514360661178224325180053710937500000000000000000000000000000000000000000000000000000*y^5*x^10+6968516008508047637704263622380971846183737178981750860214233398437500000000000000000000000000000000000000000000000000*y^5*x^9+394286132828674423385187718743018108844757080078125000000000000000000000000000000000000000000000000000000000000000000000000000000000000*y^5*x^16+8040278401656412373832334403631687164306640625000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000*y^6*x^17+19943372879042413328808957346643205302129483685088707825488433837890625000000000000000000000000000000000000000*y^6*x^5+15330655154855127952037010177735378916559986681523496696178436279296875000000000000000000000000000000000000000000*y^6*x^6+9575467310380560461038235932841538830811168249353755265665054321289062500000000000000000000000000000000000000000000*y^6*x^7+4947227579330178774627876330594971633814946460546321389675140380859375000000000000000000000000000000000000000000000000*y^6*x^8+475955313625551990713500635367065111398696899414062500000000000000000000000000000000000000000000000000000000000000000000000000000000000*y^6*x^15+2865172578258321272505971695755495395543575286865234375000000000000000000000000000000000000000000000000000000000000000000000000000000*y^6*x^14+14730331002077230084269719730305324481707453727722167968750000000000000000000000000000000000000000000000000000000000000000000000000*y^6*x^13+64793171143369703462501570416749855018602477788925170898437500000000000000000000000000000000000000000000000000000000000000000000*y^6*x^12+243823536373380887438033400195261325392206592080593109130859375000000000000000000000000000000000000000000000000000000000000000*y^6*x^11+783471320564821753791528646919824033895224420338797569274902343750000000000000000000000000000000000000000000000000000000000*y^6*x^10+2141313370168082319413239834776211777327215707213229656219482421875000000000000000000000000000000000000000000000000000000*y^6*x^9+67269444372328165993956856520542669296264648437500000000000000000000000000000000000000000000000000000000000000000000000000000000000000000*y^6*x^16+6011188285900138568540988008845032193879154505671110505481719970703125000000000000000000000000000000000000000000*y^7*x^5+4352055277821408266350032449937609680084237927460147336959838867187500000000000000000000000000000000000000000000000*y^7*x^6+2552921595538700394659546119809692289955235357219398465156555175781250000000000000000000000000000000000000000000000000*y^7*x^7+1234864362141330462313321780327800569314741032748962640762329101562500000000000000000000000000000000000000000000000000000*y^7*x^8+65682066751565277685527965521548771858215332031250000000000000000000000000000000000000000000000000000000000000000000000000000000000000000*y^7*x^15+438816052060388429713089056589054858922958374023437500000000000000000000000000000000000000000000000000000000000000000000000000000000000*y^7*x^14+2483101557927140562065415139135833340871334075927734375000000000000000000000000000000000000000000000000000000000000000000000000000000*y^7*x^13+11938057601694546962729174247927094720802378654479980468750000000000000000000000000000000000000000000000000000000000000000000000000*y^7*x^12+48811195056106558254705917613744825298478397130966186523437500000000000000000000000000000000000000000000000000000000000000000000*y^7*x^11+169541195131718106365592699742533555242184653632640838623046875000000000000000000000000000000000000000000000000000000000000000*y^7*x^10+498646794609674868181866148723066432467924959318804740905761718750000000000000000000000000000000000000000000000000000000000*y^7*x^9+8281152270798709796682101071500778198242187500000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000*y^7*x^16+1405807780118441938403318056869113802397723036773709760570526123046875000000000000000000000000000000000000000000000*y^8*x^5+955230576785575447799622728459628678333599851781182374954223632812500000000000000000000000000000000000000000000000000*y^8*x^6+524245819475872935581307877220856361664606241361436486244201660156250000000000000000000000000000000000000000000000000000*y^8*x^7+236415397172860121768182823370287286871083155244976282119750976562500000000000000000000000000000000000000000000000000000000*y^8*x^8+6616353691436821717600317271227240562438964843750000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000*y^8*x^15+49584638268632137199964022241948491334915161132812500000000000000000000000000000000000000000000000000000000000000000000000000000000000000*y^8*x^14+311600853195888010207279323019575394690036773681640625000000000000000000000000000000000000000000000000000000000000000000000000000000000*y^8*x^13+1649982082680167648673515868055409748612046241760253906250000000000000000000000000000000000000000000000000000000000000000000000000000*y^8*x^12+7378714448978601427582113276029678290670496225357055664062500000000000000000000000000000000000000000000000000000000000000000000000*y^8*x^11+27865745000886959424903831831051469039215506136417388916015625000000000000000000000000000000000000000000000000000000000000000000*y^8*x^10+88652819259316089037073784425003470720971039376854896545410156250000000000000000000000000000000000000000000000000000000000000*y^8*x^9+734500767754892340256013862848281860351562500000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000*y^8*x^16+70908645645691418683528900146484375000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000*y^13*x^13+1192685416612513446807861328125000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000*y^15*x^11+55799807113621965050697326660156250000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000*y^16*x^10+11746794992985682921409606933593750000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000*y^14*x^12+294119527343229083243608474731445312500000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000*y^12*x^14+10341142671565822676132130622863769531250000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000*y^11*x^14+24968203908745918733236527442932128906250000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000*y^10*x^15+482288342379842525984776678323745727539062500000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000*y^9*x^15+255506926860090431296529811252808622124873537095457801818847656250000000000000000000000000000000000000000000000000000*y^9*x^5+162306917656670918803432089998552736730857371562538146972656250000000000000000000000000000000000000000000000000000000000*y^9*x^6+28979199409970078950246592945617985725402832031250000000000000000000000000000000000000000000000000000000000000000000000000000000000000000*y^9*x^13+170541780619083049134351197739354198694229125976562500000000000000000000000000000000000000000000000000000000000000000000000000000000000*y^9*x^12+840622337037292964179798834143789765667915344238281250000000000000000000000000000000000000000000000000000000000000000000000000000000*y^9*x^11+3474849822571031436193508445452583049099969863891601562500000000000000000000000000000000000000000000000000000000000000000000000000*y^9*x^10+12028820873410360805514747068046079760173973798751831054687500000000000000000000000000000000000000000000000000000000000000000000*y^9*x^9+34724998656879561278532662617430350265287313916683197021484375000000000000000000000000000000000000000000000000000000000000000*y^9*x^8+82983293937163916669239955430897061442775017621183395385742187500000000000000000000000000000000000000000000000000000000000*y^9*x^7+4107916386738483861709129973857402801513671875000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000*y^9*x^14+35900687560019528551298826473918151500435313739631652832031250000000000000000000000000000000000000000000000000000000000*y^10*x^5+21227038278228296592836284776426627512152493919754028320312500000000000000000000000000000000000000000000000000000000000000*y^10*x^6+1971785072926736968500440139377117156982421875000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000*y^10*x^13+13037078500323928172151519947609639167785644531250000000000000000000000000000000000000000000000000000000000000000000000000000000000000000*y^10*x^12+71479494758942867626605903252792113065719604492187500000000000000000000000000000000000000000000000000000000000000000000000000000000000*y^10*x^11+325953564190573249158932069395673192083835601806640625000000000000000000000000000000000000000000000000000000000000000000000000000000*y^10*x^10+1236120252388399104820026027837091217595195770263671875000000000000000000000000000000000000000000000000000000000000000000000000000*y^10*x^9+3886147826066156511700042301173414826486867666244506835937500000000000000000000000000000000000000000000000000000000000000000000*y^10*x^8+10061870886295559704261481181095914378238383526802062988281250000000000000000000000000000000000000000000000000000000000000000*y^10*x^7+245725756724279105916196462392807006835937500000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000*y^10*x^14+3850019782983808235711177482807167011219822411727905273437500000000000000000000000000000000000000000000000000000000000000*y^11*x^5+722435595851420564438448645861148834228515625000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000*y^11*x^12+4454416836428993866640264569952750205993652343750000000000000000000000000000000000000000000000000000000000000000000000000000000000000000*y^11*x^11+22615975999243537948559930487286119222640991210937500000000000000000000000000000000000000000000000000000000000000000000000000000000000*y^11*x^10+94707045725196342033039966959729478514194488525390625000000000000000000000000000000000000000000000000000000000000000000000000000000*y^11*x^9+326500730909408747284712396684391066306948661804199218750000000000000000000000000000000000000000000000000000000000000000000000000*y^11*x^8+921530488210140917522822001201004440672276973724365234375000000000000000000000000000000000000000000000000000000000000000000000*y^11*x^7+2108426781387263768352630493637386012374082298278808593750000000000000000000000000000000000000000000000000000000000000000000*y^11*x^6+95967979355255888602478657960891723632812500000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000*y^11*x^13+308118492383997293871293831083556127253985652923583984375000000000000000000000000000000000000000000000000000000000000000000*y^12*x^5+731140518928607392125773429870605468750000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000*y^13*x^12+28110228734570530471623932480812072753906250000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000*y^12*x^12+5956011789461831081228929758071899414062500000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000*y^13*x^11+858466507424990087248485088348388671875000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000*y^14*x^10+38851997920297529494302445461750030517578125000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000*y^13*x^10+10717412922179424173545837402343750000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000*y^15*x^10+463937019386948959809541702270507812500000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000*y^16*x^9+74941344780044301466756820678710937500000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000*y^15*x^9+113370463586834726901769638061523437500000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000*y^14*x^11+2971906447214927179975092411041259765625000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000*y^16*x^8+412007459374282785891305112838745117187500000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000*y^15*x^8+5162381850940973164221820554733276367187500000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000*y^14*x^9+204425392092458555317682774888348579406738281250000000000000000000000000000000000000000000000000000000000000000000000000000000000000000*y^13*x^9+197550154037969817449444505611658096313476562500000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000*y^12*x^11+1129195616960682347199521095417988300323486328125000000000000000000000000000000000000000000000000000000000000000000000000000000000000000*y^12*x^10+5270709271402146391391294443267263054847717285156250000000000000000000000000000000000000000000000000000000000000000000000000000000000*y^12*x^9+24789551887290065779286412694835662841796875000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000*y^14*x^8+869521078284347904133035246312595605850219726562500000000000000000000000000000000000000000000000000000000000000000000000000000000000*y^13*x^8+20087220603742421427116644847348386377096176147460937500000000000000000000000000000000000000000000000000000000000000000000000000000*y^12*x^8+62241253299926428016585932715075110253405570983886718750000000000000000000000000000000000000000000000000000000000000000000000000*y^12*x^7+8185829103885753360953268229684206233596801757812500000000000000000000000000000000000000000000000000000000000000000000000000000*y^13*x^6+155411880811466846588579112327581539171319961547851562500000000000000000000000000000000000000000000000000000000000000000000000*y^12*x^6+2982319550235374579157616455643413224220275878906250000000000000000000000000000000000000000000000000000000000000000000000000000000*y^13*x^7+1786423000301954182133480785560607910156250000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000*y^15*x^7+57097992576601338862419163227081298828125000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000*y^16*x^6+6087235396142827412597484237487792968750000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000*y^15*x^6+169760619651267772885016052535057067871093750000000000000000000000000000000000000000000000000000000000000000000000000000000000000*y^16*x^5+16126309650557470487178846840023803710937500000000000000000000000000000000000000000000000000000000000000000000000000000000000000*y^15*x^5+95038208833468030197324098091958999633789062500000000000000000000000000000000000000000000000000000000000000000000000000000000000000*y^14*x^7+289194277983191713677191677033813095092773437500000000000000000000000000000000000000000000000000000000000000000000000000000000000*y^14*x^6+689802147069623752019023122667773573303222656250000000000000000000000000000000000000000000000000000000000000000000000000000000*y^14*x^5+17734708808973298710295640003493808144741058349609375000000000000000000000000000000000000000000000000000000000000000000000000*y^13*x^5+14784131420669592824098478555679321289062500000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000*y^16*x^7+3225394262741212993549406528472900390625000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000*y^12*x^13+110592725904786272851364667086456329822540283203125000000000000000000000000000000000000000000000000000000000000000000000000000000000000*y^3*x^18+31178686783658281254619218155774044990539550781250000000000000000000000000000000000000000000000000000000000000000000000000000000000000000*y^4*x^18+4947016877281525708043575286865234375000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000*y^8*x^18+75777632192249841103258371353149414062500000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000*y^7*x^18+805504483574650743155251671791076660156250000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000*y^6*x^18+6000015634537550225473873924362659454345703125000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000*y^5*x^18+34241008446476757783448258353397873401641845703125000000000000000000000000000000000000000000000000000000000000000000000000000000000000*y^2*x^19+721034974690949901153326456071758270263671875000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000*y*x^21+68563252099540461487267554004192352294921875000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000*y*x^22+3965164131391507143106579120227408409118652343750000000000000000000000000000000000000000000000000000000000000000000000000000000000000000*y^2*x^20+13408924405083938583057513514886283874511718750000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000*y^3*x^19+3377610364907914784048630755121707916259765625000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000*y^4*x^19+76711177825927734375000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000*y^8*x^23+8017085194587707519531250000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000*y^8*x^22+12707371053225409984588623046875000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000*y^8*x^20+287783353344089934110641479492187500000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000*y^8*x^19+5339194816227069378561973571777343750000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000*y^7*x^19+66795066052877685469540119171142578125000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000*y^6*x^19+573313423433073478775714479207992553710937500000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000*y^5*x^19+400326728721857070922851562500000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000*y^8*x^21+1387974536054033303673559725911617279052734375000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000*y^3*x^20+68187713623046875000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000*y^7*x^24+7377910614013671875000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000*y^7*x^23+12607045777819347381591796875000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000*y^7*x^21+297418227208933067321777343750000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000*y^7*x^20+4503849521784642431674003601074218750000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000*y^6*x^20+45470629447284533902035212516784667968750000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000*y^5*x^20+308524377532064845818608916640281677246093750000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000*y^4*x^20+382127222881317138671875000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000*y^7*x^22+393011088801602106949167977156639099121093750000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000*y^2*x^21+26035308837890625000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000*y^5*x^26+47731399536132812500000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000*y^6*x^25+3009160995483398437500000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000*y^5*x^25+5340666294097900390625000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000*y^6*x^24+167033812732696533203125000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000*y^5*x^24+8863952653885747504585671424865722656250000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000*y^3*x^22+33005561334220270817461417913436889648437500000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000*y^2*x^22+5927300540040373802185058593750000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000*y^5*x^23+9810773399543237686157226562500000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000*y^6*x^22+150998672265779428720474243164062500000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000*y^5*x^22+240698356742239551544189453125000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000*y^6*x^21+2939888492529790335862636566162109375000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000*y^5*x^21+1456500201571123118876218795776367187500000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000*y^4*x^22+23451511192943723830720126628875732421875000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000*y^4*x^21+121451565189936748742560593843460083007812500000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000*y^3*x^21+286534545989036560058593750000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000*y^6*x^23+5555741709590614607193674913048744201660156250000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000*x^23+95367431640625000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000*y*x^30+798881053924560546875000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000*x^30+12430191040039062500000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000*y*x^29+90587139129638671875000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000*y^2*x^28+782200412750244140625000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000*y*x^28+3337860107421875000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000*y^3*x^28+10848045349121093750000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000*y^4*x^27+410423278808593750000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000*y^3*x^27+715255737304687500000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000*y^2*x^29+1293846368789672851562500000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000*y^4*x^26+24305086727142333984375000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000*y^3*x^26+5532508187294006347656250000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000*y^2*x^27+31646798063206672668457031250000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000*y*x^27+51751813292503356933593750000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000*x^29+2158023881286382675170898437500000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000*x^28+65087762878424823284149169921875000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000*x^27+216968289755439758300781250000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000*y^2*x^26+924905691554619073867797851562500000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000*y*x^26+1512579509390543066859245300292968750000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000*x^26+28173055976082432635706663131713867187500000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000*x^25+374305482429900182069921493530273437500000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000*y*x^24+431942757997155853650200068950653076171875000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000*x^24+20798847150531265501976013183593750000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000*y*x^25+922968854705190658569335937500000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000*y^3*x^25+2726170398240280151367187500000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000*y^4*x^24+25245891877856787681579589843750000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000*y^3*x^24+72010921616599508404731750488281250000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000*y^4*x^23+529687979059695770251750946044921875000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000*y^3*x^23+6138022252907994985580444335937500000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000*y^2*x^25+133409464420846990141868591308593750000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000*y^2*x^24+2316785442327712265708088874816894531250000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000*y^2*x^23+5535820647861757518793185949325561523437500000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000*y*x^23+74220770018100738525390625000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000*y^4*x^25+22216855717799718657878177855346282990737231468180672325152136075953309326171875000000000000*x^5+10143760622958795283251174272834031222961905328211327275265648696174398842773437500000*x^3+17108861769411732152099358378553115149213862107690441163554314365394520019531250000000000*x^4+17725006203208130467619466143774248213298307071052582152499427974076633792968750000000*y*x^2+64251398048687113087434121819893753025695666793191659168571149547405249023437500000000000000*y*x^4+39722815325743092303555600787785420202076727048649620539565981706761677197265625000000000*y*x^3+33780561302583526513659623196224067419911220122034151639888406576618945751953125000000000*y^2*x^2+72577271666491952237494241492312913904998079501547778287321419105228436279296875000000000000*y^2*x^3+112387014590558551943486520444808722394579435462278010033282262099825500488281250000000000000000*y^2*x^4+39926691396401745224476043600416150601779927103145759622835489872288286132812500000000000000*y^3*x^2+82093444720391743777785592781894670766149179153680100435148575961637573242187500000000000000000*y^3*x^3+121471855927145956891673429284227939178571192750043859333049912544854736328125000000000000000000000*y^3*x^4+32746293550792920744656392475617161377570838257217043459530533697137329101562500000000000000000*y^4*x^2+64309485142658212261923079360994235598659313544407504924140952985659790039062500000000000000000000*y^4*x^3+90738864434428871379649058820576886075553196564137733435325841812591552734375000000000000000000000000*y^4*x^4+19752980375152338115775202466068671692473487717545346608610410453515625000000000000000000000000000*y^5*x^2+36973360508975595305970877168031130509954294247729183005202590519714355468750000000000000000000000000*y^5*x^3+49633131664198187654624119663402576882758346460638795057276235778808593750000000000000000000000000000000*y^5*x^4+9060640113416542201754759200408102686704034359983993557473464483337402343750000000000000000000000000*y^6*x^2+16126734148084426261913904725867418543138347743603915271347324653625488281250000000000000000000000000000*y^6*x^3+20545293502827494686710612122731987902949440497260563495530311203002929687500000000000000000000000000000000*y^6*x^4+3221943184373780786702120184056855523280266129975120476625443756103515625000000000000000000000000000000*y^7*x^2+5439105940758340677611153349277631682589218586462783851926227569580078125000000000000000000000000000000000*y^7*x^3+6558279385351508508804126647203733466352621264533104140551338195800781250000000000000000000000000000000000000*y^7*x^4+897039569100058105373239439064083501451761528306578386795517730712890625000000000000000000000000000000000*y^8*x^2+1432271663188376403574640852189426764323092704043147008070468902587890625000000000000000000000000000000000000*y^8*x^3+1629589847626759602837703738096641131766940243998823665341377258300781250000000000000000000000000000000000000000*y^8*x^4+196047352670678396667755466789034095483207099729067089617614746093750000000000000000000000000000000000000000*y^9*x^2+295146117157431573822405271116020762426333407814385356986999511718750000000000000000000000000000000000000000000*y^9*x^3+315818520342432038344738325326749167515481339769025910568237304687500000000000000000000000000000000000000000000000*y^9*x^4+33493487843918661565230880921024520278262038027313852142333984375000000000000000000000000000000000000000000000*y^10*x^2+47382013179647990341136869026463401183272337316979038238525390625000000000000000000000000000000000000000000000000*y^10*x^3+47507177192591245719626422909314573678696962722879142761230468750000000000000000000000000000000000000000000000000000*y^10*x^4+4421971426008631284014456715482902890109247966142965698242187500000000000000000000000000000000000000000000000000*y^11*x^2+5478892691455811857497515029876774446408352453273773193359375000000000000000000000000000000000000000000000000000000000*y^11*x^4+5855885233814107460658584141818558597633513230913925170898437500000000000000000000000000000000000000000000000000000*y^11*x^3+441817623518383832003048684881754527525102012432708740234375000000000000000000000000000000000000000000000000000000*y^12*x^2+473945619309471871730470928169880604802617704582214355468750000000000000000000000000000000000000000000000000000000000000*y^12*x^4+36935468825387734059924951946381500806831851959228515625000000000000000000000000000000000000000000000000000000000000000*y^13*x^3+545367670724750739776215606045925753465853559856414794921875000000000000000000000000000000000000000000000000000000000*y^12*x^3+29657463991562688990288558854208095150138740539550781250000000000000000000000000000000000000000000000000000000000000000000*y^13*x^4+32555100506218272257355772018470030212402343750000000000000000000000000000000000000000000000000000000000000000000000000000000*y^15*x^4+627041191712452507358781271596477699279785156250000000000000000000000000000000000000000000000000000000000000000000000000000*y^16*x^3+48405901440299856260395063164398576202392578125000000000000000000000000000000000000000000000000000000000000000000000000000*y^15*x^3+711586842599791264120788555583908302307128906250000000000000000000000000000000000000000000000000000000000000000000000000*y^16*x^2+49987088194605322402590635600305951673583984375000000000000000000000000000000000000000000000000000000000000000000000000*y^15*x^2+1262507358056958910097248229723071440719604492187500000000000000000000000000000000000000000000000000000000000000000000000000*y^14*x^4+1712034387134124794196206848241558364121398925781250000000000000000000000000000000000000000000000000000000000000000000000*y^14*x^3+1620711170765800985324781096945868964542565917968750000000000000000000000000000000000000000000000000000000000000000000*y^14*x^2+32256889044666610620935288330081082613905940338134765625000000000000000000000000000000000000000000000000000000000000*y^13*x^2+381477666646663823502968693647127151489257812500000000000000000000000000000000000000000000000000000000000000000000000000000000*y^16*x^4+4346345705323247958793689553002528965991432708196434159950483755594623144726562500*x^2+5080521694279144220415646508549888694261776813886313802914366090337500813710937500*y*x+10086613857648328679515834138432188772600069331147453742033659999133920833007812500000*y^2*x+12439963534244366706123988660181849005595376646131072247059235517843420800781250000000000*y^3*x+10665643139566972984469872368705493485155865903130103253655448905409289550781250000000000000*y^4*x+6738988586688159112136838415718624382416486665448759665697692400694580078125000000000000000000*y^5*x+3244954089272996617495982407238434573358638448636055622097246709906005859375000000000000000000000*y^6*x+1214215088790714751139399934380048292938501861406244290910203971557617187500000000000000000000000000*y^7*x+356662984198726849713032847825224813594056237497298199369348739624023437500000000000000000000000000000*y^8*x+82476439609532889073195286609679560439261955378066188748809814453125000000000000000000000000000000000000*y^9*x+14956694796867847204307092611445809193981000249145290270385742187500000000000000000000000000000000000000000*y^10*x+2103454946046123050769622882599517766976216988990118225097656250000000000000000000000000000000000000000000000*y^11*x+224759445528736863344263524777108200985513406918313598632812500000000000000000000000000000000000000000000000000*y^12*x+498437562969602885556204954914500344085693359375000000000000000000000000000000000000000000000000000000000000000000000*y^16*x+32026578973543831756722962110588563739233398437500000000000000000000000000000000000000000000000000000000000000000000*y^15*x+956212210878096358560316671059172072400623779296875000000000000000000000000000000000000000000000000000000000000000*y^14*x+17627340562366854486357424181394430525437888773803710937500000000000000000000000000000000000000000000000000000000*y^13*x+159360963853698617381748433807656621987461855856558956480644095408610554009))/((6250*x+21) * (6250*x+6250*y+21) * (25000*x+109) * (25000*x+25000*y+59) * (50000*x+193) * (50000*x+223) * (50000*x+243) * (50000*x+253) * (50000*x+273) * (50000*x+303) * (50000*x+50000*y+143) * (50000*x+50000*y+173) * (50000*x+50000*y+193) * (50000*x+50000*y+203) * (50000*x+50000*y+223) * (50000*x+50000*y+253) * (100000*x+337) * (100000*x+387) * (100000*x+437) * (100000*x+447) * (100000*x+487) * (100000*x+507) * (100000*x+547) * (100000*x+607) * (100000*x+100000*y+237) * (100000*x+100000*y+287) * (100000*x+100000*y+337) * (100000*x+100000*y+347) * (100000*x+100000*y+387) * (100000*x+100000*y+407) * (100000*x+100000*y+447) * (100000*x+100000*y+507))

SMT

> / < Threshold

Encode as SMT/x > 0.2 and x < 0.4 and y > 0.2 and y < 0.4

//

or

[CAV 2015]


Prophesy

!46

State Elimination12

12

12

12

12

12

12

12

12

12

12

12

12

12

p

q

1�q

1�p

p

p

1�p p

1�q

p

1�p

(1�p) · q

p · q

p

p

1�p

1�q1�pq

q·(1�p)1�pq

p

q·(1�p)1�pq

p · 1�q1�pq

(1�p) · 1�q1�pq p · (1�p) · 1�q

1�pq

(1�p) · 1�q1�pq

(100000 * (5960464477539062500000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000*x^31+702373936490740872940087742602805112667874188094069949758963540019627405253125*y+1450904375022708825682321296378347076778416883393982007472009476183433015546875000*y^2+1864755946862212781696097687854559826846553823287794907364816761374121929687500000000*y^3+1668951994385017644663304962887700020242746670158135295164653664125004492187500000000000*y^4+1102865149919950107236938145739490878327656928384325737735665870684589843750000000000000000*y^5+556547137079102685146960572336091343090015799330093919477074765334472656250000000000000000000*y^6+218742892187106712970110443815793230349572908927046406971833843798828125000000000000000000000000*y^7+67657120501106251590042314841381151405530532495603704972860592041015625000000000000000000000000000*y^8+16518818139533290562094250699015259007637423958616171182550292968750000000000000000000000000000000000*y^9+3172295793253285940594791438727346168066208663418201237548828125000000000000000000000000000000000000000*y^10+474016764439910699755280957262762537268094956223410561523437500000000000000000000000000000000000000000000*y^11+54012878922764075188965754667484772073830752262641357421875000000000000000000000000000000000000000000000000*y^12+162426578488654837092788848277278964025878906250000000000000000000000000000000000000000000000000000000000000000000*y^16+9589665193970181581958253602290550036087890625000000000000000000000000000000000000000000000000000000000000000000*y^15+264718553211154172716577556561825608809590996093750000000000000000000000000000000000000000000000000000000000000*y^14+4536039578070738872212092128811920272247180719775390625000000000000000000000000000000000000000000000000000000*y^13+1197686862314302852123159115280362082895137117450174688158218156239594687237500*x+95367431640625000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000*y^15*x^16+5960464477539062500000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000*y^16*x^15+715255737304687500000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000*y^14*x^17+3337860107421875000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000*y^13*x^18+287256240844726562500000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000*y^13*x^17+7503509521484375000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000*y^15*x^15+446975231170654296875000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000*y^16*x^14+58915615081787109375000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000*y^14*x^16+11666933650970458984375000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000*y^13*x^16+276674289703369140625000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000*y^15*x^14+15642804503440856933593750000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000*y^16*x^13+2282697396278381347656250000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000*y^14*x^15+68187713623046875000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000*y^9*x^22+26035308837890625000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000*y^11*x^20+10848045349121093750000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000*y^12*x^19+47731399536132812500000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000*y^10*x^21+6874685287475585937500000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000*y^9*x^21+2432739257812500000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000*y^11*x^19+973612070083618164062500000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000*y^12*x^18+4636150836944580078125000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000*y^10*x^20+330491340312957763671875000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000*y^9*x^20+107887256336212158203125000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000*y^11*x^18+41361572020053863525390625000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000*y^12*x^17+214244310393333435058593750000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000*y^10*x^19+6264176030117511749267578125000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000*y^10*x^18+3019034684533834457397460937500000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000*y^11*x^17+10077168994217181205749511718750000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000*y^9*x^19+218679320692671780347824096679687500000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000*y^9*x^18+60793009248859964457385012553244829177856445312500000000000000000000000000000000000000000000000000000000000000000000000000000000000000*x^22+297097093148446083068847656250000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000*y^13*x^15+6345081593513488769531250000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000*y^15*x^13+338845650976896286010742187500000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000*y^16*x^12+55243594083261489868164062500000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000*y^14*x^14+1105408189623689651489257812500000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000*y^12*x^16+59778028831328625679016113281250000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000*y^11*x^16+129992351966387640714645385742187500000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000*y^10*x^17+3592059357401546746835708618164062500000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000*y^9*x^17+5314641117812264204025268554687500000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000*y^13*x^14+101276044196971893310546875000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000*y^15*x^12+5079412310205996036529541015625000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000*y^16*x^11+935117828937297344207763671875000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000*y^14*x^13+20832672803782986998558044433593750000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000*y^12*x^15+890128854396262941949367523193359375000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000*y^11*x^15+2035648911116343191161155700683593750000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000*y^10*x^16+571901558644897434730104612251580536365509033203125000000000000000000000000000000000000000000000000000000000000000000000000000000000*x^21+6505156213774121289062116393951794624328613281250000000000000000000000000000000000000000000000000000000000000000000000000000000000000*y*x^20+4662278864207081485787459450836753695607185363769531250000000000000000000000000000000000000000000000000000000000000000000000000000*x^20+50740949360382704311506607784522055442333221435546875000000000000000000000000000000000000000000000000000000000000000000000000000000*y*x^19+33135167684433827765543742066794036569982767105102539062500000000000000000000000000000000000000000000000000000000000000000000000*x^19+254988182506988181965992574576107686781883239746093750000000000000000000000000000000000000000000000000000000000000000000000000000000*y^2*x^18+344159703420344416488877511691944861498808860778808593750000000000000000000000000000000000000000000000000000000000000000000000000*y*x^18+206214676427110066935520381227559859435559809207916259765625000000000000000000000000000000000000000000000000000000000000000000*x^18+1646504023832025205043527293258199844966387748718261718750000000000000000000000000000000000000000000000000000000000000000000000000*y^2*x^17+2038299011679168681536786940969947305159554958343505859375000000000000000000000000000000000000000000000000000000000000000000000*y*x^17+1127322211389075632261649358486635636727344074845314025878906250000000000000000000000000000000000000000000000000000000000000*x^17+10570641372121521126599008680635038021300526442527770996093750000000000000000000000000000000000000000000000000000000000000000*y*x^16+5424244866822483211169983239665545598525955378729104995727539062500000000000000000000000000000000000000000000000000000000*x^16+22993645001020890980508212500416188083495861348173260688781738281250000000000000000000000000000000000000000000000000000*x^15+23106452601151809446728665574330661998398492974563961554050901851429382324218750000000000000000*x^6+282220375348493449273670496972815526950749696894880327939987182617187500000000000000000000000000000000000000000000*x^13+814633149719803971693797397545495451586256966581923839750289916992187500000000000000000000000000000000000000000*x^12+2058599763340274458813037963225830507637034015959815951823577880859375000000000000000000000000000000000000000*x^11+4533805972571849662940067537110289096231331477929786871111489105224609375000000000000000000000000000000000*x^10+8649701137732929064620802335522190772707045156810048754059383544921875000000000000000000000000000000000*x^9+14180901742716694228717298441261618573233200286918166438183461530303955078125000000000000000000000000*x^8+19768861305011757896070993030413059018237150485074765068083490613479614257812500000000000000000000*x^7+85869491666048514675621071964575286298115481225557267665863037109375000000000000000000000000000000000000000000000000*x^14+191895690942957145060818410577251915767042894042200326919555664062500000000000000000000000000000000000000000000000000000*y*x^14+48079588734342979484628751087990163633884616566300392150878906250000000000000000000000000000000000000000000000000000000000*y*x^15+45384594749684045248248501666837650848126535875797271728515625000000000000000000000000000000000000000000000000000000000000000*y^2*x^15+9254240254410034438239473752839744703664484977722167968750000000000000000000000000000000000000000000000000000000000000000000000*y^2*x^16+4808497825168630622016252118027737164762735366821289062500000000000000000000000000000000000000000000000000000000000000000000000000*y^3*x^16+46374914847573314725006580352783203125000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000*y^9*x^16+784364818915966487290409399699586237983703613281250000000000000000000000000000000000000000000000000000000000000000000000000000000000*y^3*x^17+67045466910621389508135652542114257812500000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000*y^8*x^17+872076472686334922296215642452239990234375000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000*y^7*x^17+245018943113270535598234591607177663326263427734375000000000000000000000000000000000000000000000000000000000000000000000000000000000000*y^4*x^17+79902743234754692159260734931659212814437866188681696936262094202117187500000000000000000000000*y*x^5+2058388546930028807324019289544624516121047555182549962806701660156250000000000000000000000000000000000000000000000*y*x^12+5506851751618149843363906448107815507953028740648907079851150512695312500000000000000000000000000000000000000000*y*x^11+12807247187088686914338391857783851884492821833877706586489334106445312500000000000000000000000000000000000000*y*x^10+25742607016468278932641491372187893805127162473967283923154634094238281250000000000000000000000000000000000*y*x^9+44371055242652867795503092118448908537712483766161666436504594360351562500000000000000000000000000000000*y*x^8+64906142572960669729859529604595439687379222830032978488770055224609375000000000000000000000000000000*y*x^7+79465409804267522774613831022256502962794062951074915474482420099713134765625000000000000000000000*y*x^6+133601786703964552750515904364324487821025900771270094244217816299047851562500000000000000000000000*y^2*x^5+671683345508612089491617428580030609830506687459852523803710937500000000000000000000000000000000000000000000000000000*y*x^13+126804776643925610425540969385337176654522315969291454715560976464843750000000000000000000000000000000*y^2*x^6+727628730541493693294188380638800119268188448705618381500244140625000000000000000000000000000000000000000000000000000000*y^2*x^13+2375685088897297207735504135658994909337962986691096575260162353515625000000000000000000000000000000000000000000000000*y^2*x^12+6750246046773726005122590874964537730741206539367203780508041381835937500000000000000000000000000000000000000000000*y^2*x^11+16626570682539104226355300337081519429172653691513843926263809204101562500000000000000000000000000000000000000000*y^2*x^10+35303984001273922226098906036792076605763693898989773322803993225097656250000000000000000000000000000000000000*y^2*x^9+64134307895667165393893134183962415029815169386270539663758579254150390625000000000000000000000000000000000*y^2*x^8+98668702060515029959436978960893000212231232499505306616099172836303710937500000000000000000000000000000*y^2*x^7+194433184541764160647176467328217745945953313156771659851074218750000000000000000000000000000000000000000000000000000000000*y^2*x^14+137755828867665398672868456205884754341941356483945271934910764510498046875000000000000000000000000000*y^3*x^5+124508137770209774402304480156271697628959743589635734016490637908935546875000000000000000000000000000000*y^3*x^6+92079775035876162038938923711207896791858960081052671638744561767578125000000000000000000000000000000000000*y^3*x^7+118155113154753037951073599559724714450188514454364776611328125000000000000000000000000000000000000000000000000000000000000000*y^3*x^14+474821985908667380519463648565926836830656141073346138000488281250000000000000000000000000000000000000000000000000000000000*y^3*x^13+1658179463711531203303107461063457870539393370358817815780639648437500000000000000000000000000000000000000000000000000000*y^3*x^12+5021805579608988921634721320547764044694633563987728581428527832031250000000000000000000000000000000000000000000000000*y^3*x^11+13142513821253073560053977677176049710364323388983511804580688476562500000000000000000000000000000000000000000000000*y^3*x^10+29567180009219130466772524064258281855280416359106831868179321289062500000000000000000000000000000000000000000000*y^3*x^9+56764817443468522277548927757493675355395255550291281657042694091796875000000000000000000000000000000000000000*y^3*x^8+25568278459136748691026672317673344608972990751266479492187500000000000000000000000000000000000000000000000000000000000000000000*y^3*x^15+97949509700726451220417437112119972144411628485736585092953435691833496093750000000000000000000000000000*y^4*x^5+84104759384964618425436847926520519892323365049919644184109712600708007812500000000000000000000000000000000*y^4*x^6+58965357466983385751674874801516495945029052128731918453212223052978515625000000000000000000000000000000000000*y^4*x^7+34380605217672423132512557548877464189756113721931108717299461364746093750000000000000000000000000000000000000000*y^4*x^8+9577094991965824130456900712669496408637583255767822265625000000000000000000000000000000000000000000000000000000000000000000000000*y^4*x^15+48007139390742337283679856421835880406647019743919372558593750000000000000000000000000000000000000000000000000000000000000000000*y^4*x^14+208195283151694492398352037928465835238952309139966964721679687500000000000000000000000000000000000000000000000000000000000000*y^4*x^13+781103772141826214088891448797007105477159508373820781707763671875000000000000000000000000000000000000000000000000000000000*y^4*x^12+2531379820890875519753330475778935502016125888340784311294555664062500000000000000000000000000000000000000000000000000000*y^4*x^11+7064344972938063738616352651026386220830567792014794685840606689453125000000000000000000000000000000000000000000000000*y^4*x^10+16894164916210863465722199645920593724976870566930117427968978881835937500000000000000000000000000000000000000000000*y^4*x^9+1650567071812513487149681491416467452275753021240234375000000000000000000000000000000000000000000000000000000000000000000000000000000*y^4*x^16+52797993139591429246447771662180089950561523437500000000000000000000000000000000000000000000000000000000000000000000000000000000000000000*y^5*x^17+50874350082259317132521630282589390005402001387938029913549858093261718750000000000000000000000000000000000*y^5*x^5+41391671138796621842782167022745914837825335015792175171056480407714843750000000000000000000000000000000000000*y^5*x^6+27433131530291664545814933514630022834243814447547507835634231567382812500000000000000000000000000000000000000000*y^5*x^7+15082310508644116242478270794566427300234428055091439522743225097656250000000000000000000000000000000000000000000000*y^5*x^8+2515167399846298188814683755117121760084629058837890625000000000000000000000000000000000000000000000000000000000000000000000000000000*y^5*x^15+13764547501446347387813207753000145221716856956481933593750000000000000000000000000000000000000000000000000000000000000000000000000*y^5*x^14+64783426388405276644376733609521924428394120931625366210937500000000000000000000000000000000000000000000000000000000000000000000*y^5*x^13+262425175109029596062035938105836732422903752143383026123046875000000000000000000000000000000000000000000000000000000000000000*y^5*x^12+914131873590992531892354924267887866575313842632508277893066406250000000000000000000000000000000000000000000000000000000000*y^5*x^11+2731250803890135858352465660594905313514360661178224325180053710937500000000000000000000000000000000000000000000000000000*y^5*x^10+6968516008508047637704263622380971846183737178981750860214233398437500000000000000000000000000000000000000000000000000*y^5*x^9+394286132828674423385187718743018108844757080078125000000000000000000000000000000000000000000000000000000000000000000000000000000000000*y^5*x^16+8040278401656412373832334403631687164306640625000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000*y^6*x^17+19943372879042413328808957346643205302129483685088707825488433837890625000000000000000000000000000000000000000*y^6*x^5+15330655154855127952037010177735378916559986681523496696178436279296875000000000000000000000000000000000000000000*y^6*x^6+9575467310380560461038235932841538830811168249353755265665054321289062500000000000000000000000000000000000000000000*y^6*x^7+4947227579330178774627876330594971633814946460546321389675140380859375000000000000000000000000000000000000000000000000*y^6*x^8+475955313625551990713500635367065111398696899414062500000000000000000000000000000000000000000000000000000000000000000000000000000000000*y^6*x^15+2865172578258321272505971695755495395543575286865234375000000000000000000000000000000000000000000000000000000000000000000000000000000*y^6*x^14+14730331002077230084269719730305324481707453727722167968750000000000000000000000000000000000000000000000000000000000000000000000000*y^6*x^13+64793171143369703462501570416749855018602477788925170898437500000000000000000000000000000000000000000000000000000000000000000000*y^6*x^12+243823536373380887438033400195261325392206592080593109130859375000000000000000000000000000000000000000000000000000000000000000*y^6*x^11+783471320564821753791528646919824033895224420338797569274902343750000000000000000000000000000000000000000000000000000000000*y^6*x^10+2141313370168082319413239834776211777327215707213229656219482421875000000000000000000000000000000000000000000000000000000*y^6*x^9+67269444372328165993956856520542669296264648437500000000000000000000000000000000000000000000000000000000000000000000000000000000000000000*y^6*x^16+6011188285900138568540988008845032193879154505671110505481719970703125000000000000000000000000000000000000000000*y^7*x^5+4352055277821408266350032449937609680084237927460147336959838867187500000000000000000000000000000000000000000000000*y^7*x^6+2552921595538700394659546119809692289955235357219398465156555175781250000000000000000000000000000000000000000000000000*y^7*x^7+1234864362141330462313321780327800569314741032748962640762329101562500000000000000000000000000000000000000000000000000000*y^7*x^8+65682066751565277685527965521548771858215332031250000000000000000000000000000000000000000000000000000000000000000000000000000000000000000*y^7*x^15+438816052060388429713089056589054858922958374023437500000000000000000000000000000000000000000000000000000000000000000000000000000000000*y^7*x^14+2483101557927140562065415139135833340871334075927734375000000000000000000000000000000000000000000000000000000000000000000000000000000*y^7*x^13+11938057601694546962729174247927094720802378654479980468750000000000000000000000000000000000000000000000000000000000000000000000000*y^7*x^12+48811195056106558254705917613744825298478397130966186523437500000000000000000000000000000000000000000000000000000000000000000000*y^7*x^11+169541195131718106365592699742533555242184653632640838623046875000000000000000000000000000000000000000000000000000000000000000*y^7*x^10+498646794609674868181866148723066432467924959318804740905761718750000000000000000000000000000000000000000000000000000000000*y^7*x^9+8281152270798709796682101071500778198242187500000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000*y^7*x^16+1405807780118441938403318056869113802397723036773709760570526123046875000000000000000000000000000000000000000000000*y^8*x^5+955230576785575447799622728459628678333599851781182374954223632812500000000000000000000000000000000000000000000000000*y^8*x^6+524245819475872935581307877220856361664606241361436486244201660156250000000000000000000000000000000000000000000000000000*y^8*x^7+236415397172860121768182823370287286871083155244976282119750976562500000000000000000000000000000000000000000000000000000000*y^8*x^8+6616353691436821717600317271227240562438964843750000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000*y^8*x^15+49584638268632137199964022241948491334915161132812500000000000000000000000000000000000000000000000000000000000000000000000000000000000000*y^8*x^14+311600853195888010207279323019575394690036773681640625000000000000000000000000000000000000000000000000000000000000000000000000000000000*y^8*x^13+1649982082680167648673515868055409748612046241760253906250000000000000000000000000000000000000000000000000000000000000000000000000000*y^8*x^12+7378714448978601427582113276029678290670496225357055664062500000000000000000000000000000000000000000000000000000000000000000000000*y^8*x^11+27865745000886959424903831831051469039215506136417388916015625000000000000000000000000000000000000000000000000000000000000000000*y^8*x^10+88652819259316089037073784425003470720971039376854896545410156250000000000000000000000000000000000000000000000000000000000000*y^8*x^9+734500767754892340256013862848281860351562500000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000*y^8*x^16+70908645645691418683528900146484375000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000*y^13*x^13+1192685416612513446807861328125000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000*y^15*x^11+55799807113621965050697326660156250000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000*y^16*x^10+11746794992985682921409606933593750000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000*y^14*x^12+294119527343229083243608474731445312500000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000*y^12*x^14+10341142671565822676132130622863769531250000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000*y^11*x^14+24968203908745918733236527442932128906250000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000*y^10*x^15+482288342379842525984776678323745727539062500000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000*y^9*x^15+255506926860090431296529811252808622124873537095457801818847656250000000000000000000000000000000000000000000000000000*y^9*x^5+162306917656670918803432089998552736730857371562538146972656250000000000000000000000000000000000000000000000000000000000*y^9*x^6+28979199409970078950246592945617985725402832031250000000000000000000000000000000000000000000000000000000000000000000000000000000000000000*y^9*x^13+170541780619083049134351197739354198694229125976562500000000000000000000000000000000000000000000000000000000000000000000000000000000000*y^9*x^12+840622337037292964179798834143789765667915344238281250000000000000000000000000000000000000000000000000000000000000000000000000000000*y^9*x^11+3474849822571031436193508445452583049099969863891601562500000000000000000000000000000000000000000000000000000000000000000000000000*y^9*x^10+12028820873410360805514747068046079760173973798751831054687500000000000000000000000000000000000000000000000000000000000000000000*y^9*x^9+34724998656879561278532662617430350265287313916683197021484375000000000000000000000000000000000000000000000000000000000000000*y^9*x^8+82983293937163916669239955430897061442775017621183395385742187500000000000000000000000000000000000000000000000000000000000*y^9*x^7+4107916386738483861709129973857402801513671875000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000*y^9*x^14+35900687560019528551298826473918151500435313739631652832031250000000000000000000000000000000000000000000000000000000000*y^10*x^5+21227038278228296592836284776426627512152493919754028320312500000000000000000000000000000000000000000000000000000000000000*y^10*x^6+1971785072926736968500440139377117156982421875000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000*y^10*x^13+13037078500323928172151519947609639167785644531250000000000000000000000000000000000000000000000000000000000000000000000000000000000000000*y^10*x^12+71479494758942867626605903252792113065719604492187500000000000000000000000000000000000000000000000000000000000000000000000000000000000*y^10*x^11+325953564190573249158932069395673192083835601806640625000000000000000000000000000000000000000000000000000000000000000000000000000000*y^10*x^10+1236120252388399104820026027837091217595195770263671875000000000000000000000000000000000000000000000000000000000000000000000000000*y^10*x^9+3886147826066156511700042301173414826486867666244506835937500000000000000000000000000000000000000000000000000000000000000000000*y^10*x^8+10061870886295559704261481181095914378238383526802062988281250000000000000000000000000000000000000000000000000000000000000000*y^10*x^7+245725756724279105916196462392807006835937500000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000*y^10*x^14+3850019782983808235711177482807167011219822411727905273437500000000000000000000000000000000000000000000000000000000000000*y^11*x^5+722435595851420564438448645861148834228515625000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000*y^11*x^12+4454416836428993866640264569952750205993652343750000000000000000000000000000000000000000000000000000000000000000000000000000000000000000*y^11*x^11+22615975999243537948559930487286119222640991210937500000000000000000000000000000000000000000000000000000000000000000000000000000000000*y^11*x^10+94707045725196342033039966959729478514194488525390625000000000000000000000000000000000000000000000000000000000000000000000000000000*y^11*x^9+326500730909408747284712396684391066306948661804199218750000000000000000000000000000000000000000000000000000000000000000000000000*y^11*x^8+921530488210140917522822001201004440672276973724365234375000000000000000000000000000000000000000000000000000000000000000000000*y^11*x^7+2108426781387263768352630493637386012374082298278808593750000000000000000000000000000000000000000000000000000000000000000000*y^11*x^6+95967979355255888602478657960891723632812500000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000*y^11*x^13+308118492383997293871293831083556127253985652923583984375000000000000000000000000000000000000000000000000000000000000000000*y^12*x^5+731140518928607392125773429870605468750000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000*y^13*x^12+28110228734570530471623932480812072753906250000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000*y^12*x^12+5956011789461831081228929758071899414062500000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000*y^13*x^11+858466507424990087248485088348388671875000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000*y^14*x^10+38851997920297529494302445461750030517578125000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000*y^13*x^10+10717412922179424173545837402343750000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000*y^15*x^10+463937019386948959809541702270507812500000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000*y^16*x^9+74941344780044301466756820678710937500000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000*y^15*x^9+113370463586834726901769638061523437500000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000*y^14*x^11+2971906447214927179975092411041259765625000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000*y^16*x^8+412007459374282785891305112838745117187500000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000*y^15*x^8+5162381850940973164221820554733276367187500000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000*y^14*x^9+204425392092458555317682774888348579406738281250000000000000000000000000000000000000000000000000000000000000000000000000000000000000000*y^13*x^9+197550154037969817449444505611658096313476562500000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000*y^12*x^11+1129195616960682347199521095417988300323486328125000000000000000000000000000000000000000000000000000000000000000000000000000000000000000*y^12*x^10+5270709271402146391391294443267263054847717285156250000000000000000000000000000000000000000000000000000000000000000000000000000000000*y^12*x^9+24789551887290065779286412694835662841796875000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000*y^14*x^8+869521078284347904133035246312595605850219726562500000000000000000000000000000000000000000000000000000000000000000000000000000000000*y^13*x^8+20087220603742421427116644847348386377096176147460937500000000000000000000000000000000000000000000000000000000000000000000000000000*y^12*x^8+62241253299926428016585932715075110253405570983886718750000000000000000000000000000000000000000000000000000000000000000000000000*y^12*x^7+8185829103885753360953268229684206233596801757812500000000000000000000000000000000000000000000000000000000000000000000000000000*y^13*x^6+155411880811466846588579112327581539171319961547851562500000000000000000000000000000000000000000000000000000000000000000000000*y^12*x^6+2982319550235374579157616455643413224220275878906250000000000000000000000000000000000000000000000000000000000000000000000000000000*y^13*x^7+1786423000301954182133480785560607910156250000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000*y^15*x^7+57097992576601338862419163227081298828125000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000*y^16*x^6+6087235396142827412597484237487792968750000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000*y^15*x^6+169760619651267772885016052535057067871093750000000000000000000000000000000000000000000000000000000000000000000000000000000000000*y^16*x^5+16126309650557470487178846840023803710937500000000000000000000000000000000000000000000000000000000000000000000000000000000000000*y^15*x^5+95038208833468030197324098091958999633789062500000000000000000000000000000000000000000000000000000000000000000000000000000000000000*y^14*x^7+289194277983191713677191677033813095092773437500000000000000000000000000000000000000000000000000000000000000000000000000000000000*y^14*x^6+689802147069623752019023122667773573303222656250000000000000000000000000000000000000000000000000000000000000000000000000000000*y^14*x^5+17734708808973298710295640003493808144741058349609375000000000000000000000000000000000000000000000000000000000000000000000000*y^13*x^5+14784131420669592824098478555679321289062500000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000*y^16*x^7+3225394262741212993549406528472900390625000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000*y^12*x^13+110592725904786272851364667086456329822540283203125000000000000000000000000000000000000000000000000000000000000000000000000000000000000*y^3*x^18+31178686783658281254619218155774044990539550781250000000000000000000000000000000000000000000000000000000000000000000000000000000000000000*y^4*x^18+4947016877281525708043575286865234375000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000*y^8*x^18+75777632192249841103258371353149414062500000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000*y^7*x^18+805504483574650743155251671791076660156250000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000*y^6*x^18+6000015634537550225473873924362659454345703125000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000*y^5*x^18+34241008446476757783448258353397873401641845703125000000000000000000000000000000000000000000000000000000000000000000000000000000000000*y^2*x^19+721034974690949901153326456071758270263671875000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000*y*x^21+68563252099540461487267554004192352294921875000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000*y*x^22+3965164131391507143106579120227408409118652343750000000000000000000000000000000000000000000000000000000000000000000000000000000000000000*y^2*x^20+13408924405083938583057513514886283874511718750000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000*y^3*x^19+3377610364907914784048630755121707916259765625000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000*y^4*x^19+76711177825927734375000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000*y^8*x^23+8017085194587707519531250000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000*y^8*x^22+12707371053225409984588623046875000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000*y^8*x^20+287783353344089934110641479492187500000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000*y^8*x^19+5339194816227069378561973571777343750000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000*y^7*x^19+66795066052877685469540119171142578125000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000*y^6*x^19+573313423433073478775714479207992553710937500000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000*y^5*x^19+400326728721857070922851562500000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000*y^8*x^21+1387974536054033303673559725911617279052734375000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000*y^3*x^20+68187713623046875000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000*y^7*x^24+7377910614013671875000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000*y^7*x^23+12607045777819347381591796875000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000*y^7*x^21+297418227208933067321777343750000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000*y^7*x^20+4503849521784642431674003601074218750000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000*y^6*x^20+45470629447284533902035212516784667968750000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000*y^5*x^20+308524377532064845818608916640281677246093750000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000*y^4*x^20+382127222881317138671875000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000*y^7*x^22+393011088801602106949167977156639099121093750000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000*y^2*x^21+26035308837890625000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000*y^5*x^26+47731399536132812500000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000*y^6*x^25+3009160995483398437500000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000*y^5*x^25+5340666294097900390625000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000*y^6*x^24+167033812732696533203125000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000*y^5*x^24+8863952653885747504585671424865722656250000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000*y^3*x^22+33005561334220270817461417913436889648437500000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000*y^2*x^22+5927300540040373802185058593750000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000*y^5*x^23+9810773399543237686157226562500000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000*y^6*x^22+150998672265779428720474243164062500000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000*y^5*x^22+240698356742239551544189453125000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000*y^6*x^21+2939888492529790335862636566162109375000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000*y^5*x^21+1456500201571123118876218795776367187500000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000*y^4*x^22+23451511192943723830720126628875732421875000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000*y^4*x^21+121451565189936748742560593843460083007812500000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000*y^3*x^21+286534545989036560058593750000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000*y^6*x^23+5555741709590614607193674913048744201660156250000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000*x^23+95367431640625000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000*y*x^30+798881053924560546875000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000*x^30+12430191040039062500000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000*y*x^29+90587139129638671875000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000*y^2*x^28+782200412750244140625000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000*y*x^28+3337860107421875000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000*y^3*x^28+10848045349121093750000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000*y^4*x^27+410423278808593750000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000*y^3*x^27+715255737304687500000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000*y^2*x^29+1293846368789672851562500000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000*y^4*x^26+24305086727142333984375000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000*y^3*x^26+5532508187294006347656250000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000*y^2*x^27+31646798063206672668457031250000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000*y*x^27+51751813292503356933593750000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000*x^29+2158023881286382675170898437500000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000*x^28+65087762878424823284149169921875000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000*x^27+216968289755439758300781250000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000*y^2*x^26+924905691554619073867797851562500000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000*y*x^26+1512579509390543066859245300292968750000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000*x^26+28173055976082432635706663131713867187500000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000*x^25+374305482429900182069921493530273437500000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000*y*x^24+431942757997155853650200068950653076171875000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000*x^24+20798847150531265501976013183593750000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000*y*x^25+922968854705190658569335937500000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000*y^3*x^25+2726170398240280151367187500000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000*y^4*x^24+25245891877856787681579589843750000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000*y^3*x^24+72010921616599508404731750488281250000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000*y^4*x^23+529687979059695770251750946044921875000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000*y^3*x^23+6138022252907994985580444335937500000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000*y^2*x^25+133409464420846990141868591308593750000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000*y^2*x^24+2316785442327712265708088874816894531250000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000*y^2*x^23+5535820647861757518793185949325561523437500000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000*y*x^23+74220770018100738525390625000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000*y^4*x^25+22216855717799718657878177855346282990737231468180672325152136075953309326171875000000000000*x^5+10143760622958795283251174272834031222961905328211327275265648696174398842773437500000*x^3+17108861769411732152099358378553115149213862107690441163554314365394520019531250000000000*x^4+17725006203208130467619466143774248213298307071052582152499427974076633792968750000000*y*x^2+64251398048687113087434121819893753025695666793191659168571149547405249023437500000000000000*y*x^4+39722815325743092303555600787785420202076727048649620539565981706761677197265625000000000*y*x^3+33780561302583526513659623196224067419911220122034151639888406576618945751953125000000000*y^2*x^2+72577271666491952237494241492312913904998079501547778287321419105228436279296875000000000000*y^2*x^3+112387014590558551943486520444808722394579435462278010033282262099825500488281250000000000000000*y^2*x^4+39926691396401745224476043600416150601779927103145759622835489872288286132812500000000000000*y^3*x^2+82093444720391743777785592781894670766149179153680100435148575961637573242187500000000000000000*y^3*x^3+121471855927145956891673429284227939178571192750043859333049912544854736328125000000000000000000000*y^3*x^4+32746293550792920744656392475617161377570838257217043459530533697137329101562500000000000000000*y^4*x^2+64309485142658212261923079360994235598659313544407504924140952985659790039062500000000000000000000*y^4*x^3+90738864434428871379649058820576886075553196564137733435325841812591552734375000000000000000000000000*y^4*x^4+19752980375152338115775202466068671692473487717545346608610410453515625000000000000000000000000000*y^5*x^2+36973360508975595305970877168031130509954294247729183005202590519714355468750000000000000000000000000*y^5*x^3+49633131664198187654624119663402576882758346460638795057276235778808593750000000000000000000000000000000*y^5*x^4+9060640113416542201754759200408102686704034359983993557473464483337402343750000000000000000000000000*y^6*x^2+16126734148084426261913904725867418543138347743603915271347324653625488281250000000000000000000000000000*y^6*x^3+20545293502827494686710612122731987902949440497260563495530311203002929687500000000000000000000000000000000*y^6*x^4+3221943184373780786702120184056855523280266129975120476625443756103515625000000000000000000000000000000*y^7*x^2+5439105940758340677611153349277631682589218586462783851926227569580078125000000000000000000000000000000000*y^7*x^3+6558279385351508508804126647203733466352621264533104140551338195800781250000000000000000000000000000000000000*y^7*x^4+897039569100058105373239439064083501451761528306578386795517730712890625000000000000000000000000000000000*y^8*x^2+1432271663188376403574640852189426764323092704043147008070468902587890625000000000000000000000000000000000000*y^8*x^3+1629589847626759602837703738096641131766940243998823665341377258300781250000000000000000000000000000000000000000*y^8*x^4+196047352670678396667755466789034095483207099729067089617614746093750000000000000000000000000000000000000000*y^9*x^2+295146117157431573822405271116020762426333407814385356986999511718750000000000000000000000000000000000000000000*y^9*x^3+315818520342432038344738325326749167515481339769025910568237304687500000000000000000000000000000000000000000000000*y^9*x^4+33493487843918661565230880921024520278262038027313852142333984375000000000000000000000000000000000000000000000*y^10*x^2+47382013179647990341136869026463401183272337316979038238525390625000000000000000000000000000000000000000000000000*y^10*x^3+47507177192591245719626422909314573678696962722879142761230468750000000000000000000000000000000000000000000000000000*y^10*x^4+4421971426008631284014456715482902890109247966142965698242187500000000000000000000000000000000000000000000000000*y^11*x^2+5478892691455811857497515029876774446408352453273773193359375000000000000000000000000000000000000000000000000000000000*y^11*x^4+5855885233814107460658584141818558597633513230913925170898437500000000000000000000000000000000000000000000000000000*y^11*x^3+441817623518383832003048684881754527525102012432708740234375000000000000000000000000000000000000000000000000000000*y^12*x^2+473945619309471871730470928169880604802617704582214355468750000000000000000000000000000000000000000000000000000000000000*y^12*x^4+36935468825387734059924951946381500806831851959228515625000000000000000000000000000000000000000000000000000000000000000*y^13*x^3+545367670724750739776215606045925753465853559856414794921875000000000000000000000000000000000000000000000000000000000*y^12*x^3+29657463991562688990288558854208095150138740539550781250000000000000000000000000000000000000000000000000000000000000000000*y^13*x^4+32555100506218272257355772018470030212402343750000000000000000000000000000000000000000000000000000000000000000000000000000000*y^15*x^4+627041191712452507358781271596477699279785156250000000000000000000000000000000000000000000000000000000000000000000000000000*y^16*x^3+48405901440299856260395063164398576202392578125000000000000000000000000000000000000000000000000000000000000000000000000000*y^15*x^3+711586842599791264120788555583908302307128906250000000000000000000000000000000000000000000000000000000000000000000000000*y^16*x^2+49987088194605322402590635600305951673583984375000000000000000000000000000000000000000000000000000000000000000000000000*y^15*x^2+1262507358056958910097248229723071440719604492187500000000000000000000000000000000000000000000000000000000000000000000000000*y^14*x^4+1712034387134124794196206848241558364121398925781250000000000000000000000000000000000000000000000000000000000000000000000*y^14*x^3+1620711170765800985324781096945868964542565917968750000000000000000000000000000000000000000000000000000000000000000000*y^14*x^2+32256889044666610620935288330081082613905940338134765625000000000000000000000000000000000000000000000000000000000000*y^13*x^2+381477666646663823502968693647127151489257812500000000000000000000000000000000000000000000000000000000000000000000000000000000*y^16*x^4+4346345705323247958793689553002528965991432708196434159950483755594623144726562500*x^2+5080521694279144220415646508549888694261776813886313802914366090337500813710937500*y*x+10086613857648328679515834138432188772600069331147453742033659999133920833007812500000*y^2*x+12439963534244366706123988660181849005595376646131072247059235517843420800781250000000000*y^3*x+10665643139566972984469872368705493485155865903130103253655448905409289550781250000000000000*y^4*x+6738988586688159112136838415718624382416486665448759665697692400694580078125000000000000000000*y^5*x+3244954089272996617495982407238434573358638448636055622097246709906005859375000000000000000000000*y^6*x+1214215088790714751139399934380048292938501861406244290910203971557617187500000000000000000000000000*y^7*x+356662984198726849713032847825224813594056237497298199369348739624023437500000000000000000000000000000*y^8*x+82476439609532889073195286609679560439261955378066188748809814453125000000000000000000000000000000000000*y^9*x+14956694796867847204307092611445809193981000249145290270385742187500000000000000000000000000000000000000000*y^10*x+2103454946046123050769622882599517766976216988990118225097656250000000000000000000000000000000000000000000000*y^11*x+224759445528736863344263524777108200985513406918313598632812500000000000000000000000000000000000000000000000000*y^12*x+498437562969602885556204954914500344085693359375000000000000000000000000000000000000000000000000000000000000000000000*y^16*x+32026578973543831756722962110588563739233398437500000000000000000000000000000000000000000000000000000000000000000000*y^15*x+956212210878096358560316671059172072400623779296875000000000000000000000000000000000000000000000000000000000000000*y^14*x+17627340562366854486357424181394430525437888773803710937500000000000000000000000000000000000000000000000000000000*y^13*x+159360963853698617381748433807656621987461855856558956480644095408610554009))/((6250*x+21) * (6250*x+6250*y+21) * (25000*x+109) * (25000*x+25000*y+59) * (50000*x+193) * (50000*x+223) * (50000*x+243) * (50000*x+253) * (50000*x+273) * (50000*x+303) * (50000*x+50000*y+143) * (50000*x+50000*y+173) * (50000*x+50000*y+193) * (50000*x+50000*y+203) * (50000*x+50000*y+223) * (50000*x+50000*y+253) * (100000*x+337) * (100000*x+387) * (100000*x+437) * (100000*x+447) * (100000*x+487) * (100000*x+507) * (100000*x+547) * (100000*x+607) * (100000*x+100000*y+237) * (100000*x+100000*y+287) * (100000*x+100000*y+337) * (100000*x+100000*y+347) * (100000*x+100000*y+387) * (100000*x+100000*y+407) * (100000*x+100000*y+447) * (100000*x+100000*y+507))

SMT

> / < Threshold

Encode as SMT/ x > 0.2 and x < 0.4 and y > 0.2 and y < 0.4

//

orSampling

Region Generation


!48


!49


Complexity

• Definitely in the existential theory of the reals (ETR), see earlier.

Thus, in PSPACE.

• Via rational function: number of variables == number of parameters

Thus, as ETR is polynomial for fixed variables, PTIME for fixed number of parameters (graph-preserving)

• With two objectives: NP-hard (graph-preserving) • NP-hard (non-graph preserving)

Also known to be SQRS-hard (graph-preserving)

!50

Facts

Does there exist a parameter valuation such that the induced MC induces probability larger than 1/2?


Checking Regions w SMT

!51

Obtaining Rational Function function is typically huge

SMT performance unpredictable

Rational function is exact everywhere

Hard to develop heuristics

Solver does too much work

#4 parameters seems out of reach


Checking Regions w/o SMT

!52

pMC is a 1.5 player game

pMC is a set of instantiated DTMCs

For all points u in the region:

Probability in DTMC(u) < Threshold?

[ATVA 2016]


2 Main Ideas

!53

1 2

[ATVA 2016]


Relaxation

!54

p1�p

s1

s5

s6 s7

p

p

q

1�q

1�p

1�p 1�p

p

s3 s4

s2

q

1�q

1�p

p

z1�z

s3 s4

s2

q

1�q

1�p

p

z1�z

[ATVA 2016]


Relaxed Markov Chain

!55

all parameters occur at most at 1 state;

and within each label with at most degree 1

reachability is maximised at extremal values

(1�z) · 1�q1�pqP( )= s3 s4

s2q

1�q

1�p

p

z1�z

[ATVA 2016]


2 Main Ideas

!56

Relaxation Lifting

2s3 s4

s2q

1�q

1�p

p

z1�z

[ATVA 2016]


Parameter Lifting

!57

s3 s4

s2q

1�q

1�p

p

z1�z

s3 s4

s2

p, z 2 [0.1, 0.3]q 2 [0.4, 0.6] q 2 {0.4, 0.6}

p, z 2 {0.1, 0.3}

0.3

0.1

0.3

0.1

0.7

0.90.7 0.9

0.60.4

0.6

0.4

We obtain an MDP

[ATVA 2016]

s3 s4

s2

0.3

0.1

0.3

0.1

0.7

0.90.7 0.9

0.6

0.40.6

0.4


2 Main Ideas

!58

Relaxation Lifting

s3 s4

s2q

1�q

1�p

p

z1�z

[ATVA 2016]

s3 s4

s2

0.3

0.1

0.3

0.1

0.7

0.90.7 0.9

0.6

0.40.6

0.4


1 Step

!59

Lifting

Lifting ( Relaxation ( D ) ) = Lifting ( D )

[ATVA 2016]

s3 s4

s2

0.3

0.1

0.3

0.1

0.7

0.90.7 0.9

0.6

0.40.6

0.4


Checking Regions

!60

Lifting

12

12

12

12

12

12

12

12

12

12

12

12

12

12

Model checking or

/pDTMC

MDP

[ATVA 2016]

00

00

000 0

00 0

0


Parameter Lifting Performance

!61

[ATVA 2016]


Parameter Lifting Performance

!62

Covering 95%

[ATVA 2016]SMT TO (1h) everywhere



So far, three options have been considered in the literature




!63


Finding satisfactory parameter valuations

A more practical approach

• Methods so far are limited to ~10 parameters. • Applications as e.g. originating from control under partial observability require

thousands of parameters.

!64

Only care for some satisfactory pointCare for all points


Curse of dimensionality

In more than 100 dimensions, sampling becomes a challenge.

• Sampling via model checking instantiated Markov chains. • Select sampling points via, e.g., particle swarm optimisation: Fitness via model

checking result. • Neglects much of the underlying structure.

!65

Use (non)linear optimisation? Convex optimisation problems use structure more

pMCs typically are not convex NLPs

Solution: Linearise concave part, boost with model checking


Empirical results

!66

[ATVA 18]

Date post:	18-Oct-2021
Category:	Documents
Upload:	others
View:	2 times
Download:	0 times

parametric systems lecture - RWTH Aachen University

Documents