Merge branch 'master' into menu_games

CMakeLists.txt

@@ -79,8 +79,8 @@ if(STORM_COMPILE_WITH_CCACHE)
 	endif()
 endif()
 
-# Base path for test files
-set(STORM_CPP_TESTS_BASE_PATH "${PROJECT_SOURCE_DIR}/src/test")
+# Directory for test resources.
+set(STORM_TEST_RESOURCES_DIR "${PROJECT_SOURCE_DIR}/resources/examples/testfiles")
 
 # Auto-detect operating system.
 set(MACOSX 0)

resources/examples/testfiles/dtmc/die.pm

@@ -29,4 +29,4 @@ label "three" = s=7&d=3;
 label "four" = s=7&d=4;
 label "five" = s=7&d=5;
 label "six" = s=7&d=6;
-label "end" = s=7;
+label "done" = s=7;

resources/examples/testfiles/lab/die.lab

@@ -0,0 +1,10 @@
+#DECLARATION
+init deadlock one two three four five six done
+#END
+0 init
+7 one done
+8 two done
+9 three done
+10 four done
+11 five done
+12 six done

resources/examples/testfiles/lab/leader4.lab

@@ -0,0 +1,8 @@
+#DECLARATION
+init deadlock elected
+#END
+0 init
+2595 elected
+2596 elected
+2599 elected
+2969 elected

resources/examples/testfiles/lab/leader4_8.lab

@@ -0,0 +1,5 @@
+#DECLARATION
+init deadlock elected
+#END
+0 init
+12399 elected

resources/examples/testfiles/lab/tiny1.lab

@@ -0,0 +1,7 @@
+#DECLARATION
+init goal
+#END
+0 init
+7 goal
+8 goal
+

resources/examples/testfiles/lab/tiny2.lab

@@ -0,0 +1,7 @@
+#DECLARATION
+init goal
+#END
+0 init
+7 goal
+8 goal
+

resources/examples/testfiles/lab/two_dice.lab

@@ -0,0 +1,40 @@
+#DECLARATION
+init deadlock done two three four five six seven eight nine ten eleven twelve
+#END
+0 init
+98 done two
+99 done three
+100 done four
+101 done five
+102 done six
+103 done seven
+111 done three
+112 done four
+113 done five
+114 done six
+115 done seven
+116 done eight
+124 done four
+125 done five
+126 done six
+127 done seven
+128 done eight
+129 done nine
+137 done five
+138 done six
+139 done seven
+140 done eight
+141 done nine
+142 done ten
+150 done six
+151 done seven
+152 done eight
+153 done nine
+154 done ten
+155 done eleven
+163 done seven
+164 done eight
+165 done nine
+166 done ten
+167 done eleven
+168 done twelve

resources/examples/testfiles/pdtmc/brp16_2.pm

@@ -12,6 +12,10 @@ const int MAX = 2;
 const double pL;
 const double pK;
 
+// timeouts
+const double TOMsg;
+const double TOAck;
+
 module sender
 
     s : [0..6];
@@ -135,3 +139,10 @@ module  channelL
 endmodule
 
 label "error" = s=5;
+
+rewards
+	[TO_Msg] true : TOMsg;
+	[TO_Ack] true : TOAck;
+endrewards
+
+

src/test/utility/brp16_2.pm → resources/examples/testfiles/pdtmc/brp_rewards16_2.pm

@@ -144,3 +144,5 @@ rewards
 endrewards
 
 
+
+label "target" = s=5;

src/test/parser/prism/two_dice.nm → resources/examples/testfiles/pmdp/two_dice.nm

@@ -3,6 +3,10 @@
 
 mdp
 
+//Coin Probabilities
+const double p1;
+const double p2;
+
 module die1
 
 	// local state
@@ -10,17 +14,17 @@ module die1
 	// value of the dice
 	d1 : [0..6] init 0;
 
-	[] s1=0 -> 0.5 : (s1'=1) + 0.5 : (s1'=2);
-	[] s1=1 -> 0.5 : (s1'=3) + 0.5 : (s1'=4);
-	[] s1=2 -> 0.5 : (s1'=5) + 0.5 : (s1'=6);
-	[] s1=3 -> 0.5 : (s1'=1) + 0.5 : (s1'=7) & (d1'=1);
-	[] s1=4 -> 0.5 : (s1'=7) & (d1'=2) + 0.5 : (s1'=7) & (d1'=3);
-	[] s1=5 -> 0.5 : (s1'=7) & (d1'=4) + 0.5 : (s1'=7) & (d1'=5);
-	[] s1=6 -> 0.5 : (s1'=2) + 0.5 : (s1'=7) & (d1'=6);
+	[] s1=0 -> p1 : (s1'=1) + 1-p1 : (s1'=2);
+	[] s1=1 -> p1 : (s1'=3) + 1-p1 : (s1'=4);
+	[] s1=2 -> p1 : (s1'=5) + 1-p1 : (s1'=6);
+	[] s1=3 -> p1 : (s1'=1) + 1-p1 : (s1'=7) & (d1'=1);
+	[] s1=4 -> p1 : (s1'=7) & (d1'=2) + 1-p1 : (s1'=7) & (d1'=3);
+	[] s1=5 -> p1 : (s1'=7) & (d1'=4) + 1-p1 : (s1'=7) & (d1'=5);
+	[] s1=6 -> p1 : (s1'=2) + 1-p1 : (s1'=7) & (d1'=6);
 	[] s1=7 & s2=7 -> 1: (s1'=7);
 endmodule
 
-module die2 = die1 [ s1=s2, s2=s1, d1=d2 ] endmodule
+module die2 = die1 [ s1=s2, s2=s1, d1=d2, p1=p2 ] endmodule
 
 rewards "coinflips"
 	[] s1<7 | s2<7 : 1;
@@ -38,3 +42,4 @@ label "nine" = s1=7 & s2=7 & d1+d2=9;
 label "ten" = s1=7 & s2=7 & d1+d2=10;
 label "eleven" = s1=7 & s2=7 & d1+d2=11;
 label "twelve" = s1=7 & s2=7 & d1+d2=12;
+label "doubles" = s1=7 & s2=7 & d1=d2;

resources/examples/testfiles/prctl/two_dice.prctl

@@ -0,0 +1,4 @@
+P<=0.17 [ F "doubles" ]
+
+
+

resources/examples/testfiles/rew/die.coin_flips.trans.rew

@@ -0,0 +1,14 @@
+0 1 1
+0 2 1
+1 3 1
+1 4 1
+2 5 1
+2 6 1
+3 1 1
+3 7 1
+4 8 1
+4 9 1
+5 10 1
+5 11 1
+6 2 1
+6 12 1

resources/examples/testfiles/rew/leader4.trans.rew

@@ -0,0 +1,661 @@
+1214 1 1486 1
+1215 2 1487 1
+1216 2 1488 1
+1217 1 1489 1
+1218 2 1490 1
+1219 1 1491 1
+1220 1 1492 1
+1221 2 1493 1
+1222 3 1494 1
+1223 3 1495 1
+1224 2 1496 1
+1225 2 1497 1
+1226 2 1498 1
+1227 2 1499 1
+1228 2 1500 1
+1229 2 1501 1
+1230 3 1502 1
+1231 3 1503 1
+1232 2 1504 1
+1233 2 1505 1
+1234 2 1506 1
+1235 2 1507 1
+1236 2 1508 1
+1237 2 1509 1
+1238 2 1510 1
+1239 2 1511 1
+1240 1 1512 1
+1241 2 1513 1
+1242 2 1514 1
+1243 2 1384 1
+1244 2 1385 1
+1245 2 1386 1
+1246 1 1387 1
+1247 1 1388 1
+1248 1 1389 1
+1249 1 1390 1
+1250 1 1391 1
+1251 1 1392 1
+1252 1 1393 1
+1253 2 1394 1
+1254 2 1395 1
+1255 1 1396 1
+1256 1 1397 1
+1257 1 1398 1
+1258 2 1399 1
+1259 2 1400 1
+1260 1 1401 1
+1261 1 1402 1
+1262 1 1403 1
+1263 1 1404 1
+1264 1 1405 1
+1265 1 1406 1
+1266 2 1407 1
+1267 2 1408 1
+1268 1 1409 1
+1269 1 1410 1
+1270 1 1411 1
+1271 1 1515 1
+1272 1 1516 1
+1273 2 1517 1
+1274 2 1518 1
+1275 2 1519 1
+1276 2 1520 1
+1277 1 1521 1
+1278 2 1522 1
+1279 2 1523 1
+1280 2 1524 1
+1281 2 1525 1
+1282 1 1526 1
+1283 1 1527 1
+1284 1 1528 1
+1285 3 1529 1
+1286 3 1530 1
+1287 2 1531 1
+1288 2 1532 1
+1289 2 1533 1
+1290 2 1534 1
+1291 2 1535 1
+1292 2 1536 1
+1293 3 1537 1
+1294 3 1538 1
+1295 2 1539 1
+1296 2 1540 1
+1297 2 1541 1
+1298 2 1542 1
+1299 2 1543 1
+1300 2 1544 1
+1301 2 1545 1
+1302 2 1546 1
+1303 1 1547 1
+1304 2 1548 1
+1305 2 1549 1
+1306 2 1384 1
+1307 2 1385 1
+1308 2 1386 1
+1309 1 1387 1
+1310 1 1388 1
+1311 1 1389 1
+1312 1 1390 1
+1313 1 1391 1
+1314 1 1392 1
+1315 2 1394 1
+1316 2 1395 1
+1317 1 1396 1
+1318 1 1397 1
+1319 1 1398 1
+1320 2 1399 1
+1321 2 1400 1
+1322 1 1401 1
+1323 1 1402 1
+1324 1 1403 1
+1325 1 1404 1
+1326 1 1405 1
+1327 1 1406 1
+1328 2 1407 1
+1329 2 1408 1
+1330 1 1409 1
+1331 1 1410 1
+1332 1 1411 1
+1333 1 1579 1
+1334 1 1580 1
+1335 2 1581 1
+1336 2 1582 1
+1337 2 1583 1
+1338 2 1584 1
+1339 1 1585 1
+1340 2 1586 1
+1341 2 1587 1
+1342 2 1588 1
+1343 2 1589 1
+1344 1 1590 1
+1345 1 1591 1
+1346 1 1592 1
+1347 1 1593 1
+1348 1 1594 1
+1349 2 1595 1
+1350 2 1596 1
+1351 1 1597 1
+1352 1 1598 1
+1353 1 1599 1
+1354 1 1600 1
+1355 1 1601 1
+1356 1 1602 1
+1357 2 1603 1
+1358 2 1604 1
+1359 1 1605 1
+1360 1 1606 1
+1361 1 1607 1
+1362 1 1608 1
+1363 1 1609 1
+1364 1 1610 1
+1365 1 1611 1
+1366 1 1612 1
+1367 0 1613 1
+1368 1 1614 1
+1369 1 1615 1
+1370 1 1616 1
+1371 1 1617 1
+1372 2 1618 1
+1373 2 1619 1
+1374 2 1620 1
+1375 2 1621 1
+1376 1 1622 1
+1377 2 1623 1
+1378 2 1624 1
+1379 2 1625 1
+1380 2 1626 1
+1381 1 1627 1
+1382 1 1628 1
+1383 1 1629 1
+1644 1 141 1
+1645 2 142 1
+1646 2 143 1
+1647 2 144 1
+1648 1 145 1
+1649 1 146 1
+1650 1 147 1
+1651 2 148 1
+1652 2 149 1
+1653 2 150 1
+1654 1 151 1
+1655 1 152 1
+1656 1 153 1
+1657 1 154 1
+1658 1 155 1
+1659 2 0 1
+1660 1 1 1
+1661 1 2 1
+1662 1 3 1
+1663 1 4 1
+1664 1 5 1
+1665 1 6 1
+1666 1 7 1
+1667 0 8 1
+1668 0 9 1
+1669 0 10 1
+1670 1 11 1
+1671 1 12 1
+1672 1 13 1
+1673 1 14 1
+1674 0 15 1
+1675 0 16 1
+1676 0 17 1
+1677 1 18 1
+1678 1 19 1
+1679 1 20 1
+1680 1 21 1
+1681 1 22 1
+1682 0 23 1
+1683 0 24 1
+1684 0 25 1
+1685 1 26 1
+1686 1 27 1
+1687 1 156 1
+1688 1 157 1
+1689 1 158 1
+1690 1 159 1
+1691 2 160 1
+1692 2 161 1
+1693 2 162 1
+1694 1 163 1
+1695 1 164 1
+1696 1 165 1
+1697 2 166 1
+1698 2 167 1
+1699 2 168 1
+1700 1 169 1
+1701 1 170 1
+1702 1 171 1
+1703 1 172 1
+1704 1 173 1
+1705 2 0 1
+1706 1 1 1
+1707 1 2 1
+1708 1 3 1
+1709 1 4 1
+1710 1 5 1
+1711 1 6 1
+1712 1 7 1
+1713 0 8 1
+1714 0 9 1
+1715 0 10 1
+1716 1 11 1
+1717 1 12 1
+1718 1 13 1
+1719 1 14 1
+1720 0 15 1
+1721 0 16 1
+1722 0 17 1
+1723 1 18 1
+1724 1 19 1
+1725 1 20 1
+1726 1 21 1
+1727 1 22 1
+1728 0 23 1
+1729 0 24 1
+1730 0 25 1
+1731 1 26 1
+1732 1 27 1
+1733 1 201 1
+1734 1 202 1
+1735 1 203 1
+1736 1 204 1
+1737 1 205 1
+1738 1 206 1
+1739 1 207 1
+1740 0 208 1
+1741 0 209 1
+1742 0 210 1
+1743 1 211 1
+1744 1 212 1
+1745 1 213 1
+1746 0 214 1
+1747 0 215 1
+1748 0 216 1
+1749 0 217 1
+1750 0 218 1
+1751 1 219 1
+1752 1 220 1
+1753 1 221 1
+1754 1 222 1
+1865 3 2122 1
+1866 3 2123 1
+1867 2 2124 1
+1868 2 2125 1
+1869 2 2126 1
+1870 2 2127 1
+1871 2 2128 1
+1872 2 2129 1
+1873 3 2130 1
+1874 3 2131 1
+1875 2 2132 1
+1876 2 2133 1
+1877 2 2134 1
+1878 2 2135 1
+1879 2 2136 1
+1880 2 2137 1
+1881 2 2138 1
+1882 2 2139 1
+1883 1 2140 1
+1884 2 2141 1
+1885 2 2142 1
+1886 2 2023 1
+1887 2 2024 1
+1888 2 2025 1
+1889 1 2026 1
+1890 1 2027 1
+1891 1 2028 1
+1892 1 2029 1
+1893 1 2030 1
+1894 1 2031 1
+1895 2 2032 1
+1896 2 2033 1
+1897 1 2034 1
+1898 1 2035 1
+1899 1 2036 1
+1900 2 2037 1
+1901 2 2038 1
+1902 1 2039 1
+1903 1 2040 1
+1904 1 2041 1
+1905 1 2042 1
+1906 1 2043 1
+1907 1 2044 1
+1908 2 2045 1
+1909 2 2046 1
+1910 1 2047 1
+1911 1 2048 1
+1912 1 2049 1
+1913 1 2143 1
+1914 1 2144 1
+1915 2 2145 1
+1916 2 2146 1
+1917 2 2147 1
+1918 2 2148 1
+1919 1 2149 1
+1920 2 2150 1
+1921 2 2151 1
+1922 2 2152 1
+1923 2 2153 1
+1924 1 2154 1
+1925 1 2155 1
+1926 1 2156 1
+1927 3 2157 1
+1928 3 2158 1
+1929 2 2159 1
+1930 2 2160 1
+1931 2 2161 1
+1932 2 2162 1
+1933 2 2163 1
+1934 2 2164 1
+1935 3 2165 1
+1936 2 2166 1
+1937 2 2167 1
+1938 2 2168 1
+1939 2 2169 1
+1940 2 2170 1
+1941 2 2171 1
+1942 2 2172 1
+1943 1 2173 1
+1944 2 2174 1
+1945 2 2175 1
+1946 2 2023 1
+1947 2 2024 1
+1948 2 2025 1
+1949 1 2026 1
+1950 1 2027 1
+1951 1 2028 1
+1952 1 2029 1
+1953 1 2030 1
+1954 1 2031 1
+1955 2 2032 1
+1956 2 2033 1
+1957 1 2034 1
+1958 1 2035 1
+1959 1 2036 1
+1960 2 2037 1
+1961 1 2039 1
+1962 1 2040 1
+1963 1 2041 1
+1964 1 2042 1
+1965 1 2043 1
+1966 1 2044 1
+1967 2 2045 1
+1968 2 2046 1
+1969 1 2047 1
+1970 1 2048 1
+1971 1 2049 1
+1972 1 2205 1
+1973 1 2206 1
+1974 2 2207 1
+1975 2 2208 1
+1976 2 2209 1
+1977 2 2210 1
+1978 1 2211 1
+1979 2 2212 1
+1980 2 2213 1
+1981 2 2214 1
+1982 2 2215 1
+1983 1 2216 1
+1984 1 2217 1
+1985 1 2218 1
+1986 1 2219 1
+1987 1 2220 1
+1988 2 2221 1
+1989 2 2222 1
+1990 1 2223 1
+1991 1 2224 1
+1992 1 2225 1
+1993 1 2226 1
+1994 1 2227 1
+1995 1 2228 1
+1996 2 2229 1
+1997 2 2230 1
+1998 1 2231 1
+1999 1 2232 1
+2000 1 2233 1
+2001 1 2234 1
+2002 1 2235 1
+2003 1 2236 1
+2004 1 2237 1
+2005 1 2238 1
+2006 0 2239 1
+2007 1 2240 1
+2008 1 2241 1
+2009 1 2242 1
+2010 1 2243 1
+2011 2 2244 1
+2012 2 2245 1
+2013 2 2246 1
+2014 2 2247 1
+2015 1 2248 1
+2016 2 2249 1
+2017 2 2250 1
+2018 2 2251 1
+2019 2 2252 1
+2020 1 2253 1
+2021 1 2254 1
+2022 1 2255 1
+2300 2 142 1
+2301 2 143 1
+2302 2 144 1
+2303 1 145 1
+2304 1 146 1
+2305 1 147 1
+2306 2 148 1
+2307 2 149 1
+2308 2 150 1
+2309 1 151 1
+2310 1 152 1
+2311 1 153 1
+2312 1 154 1
+2313 1 155 1
+2314 2 0 1
+2315 1 1 1
+2316 1 2 1
+2317 1 3 1
+2318 1 4 1
+2319 1 5 1
+2320 1 6 1
+2321 1 7 1
+2322 0 8 1
+2323 0 9 1
+2324 0 10 1
+2325 1 11 1
+2326 1 12 1
+2327 1 13 1
+2328 1 14 1
+2329 0 15 1
+2330 0 16 1
+2331 0 17 1
+2332 1 18 1
+2333 1 19 1
+2334 1 20 1
+2335 1 21 1
+2336 1 22 1
+2337 0 23 1
+2338 0 24 1
+2339 0 25 1
+2340 1 26 1
+2341 1 27 1
+2342 1 156 1
+2343 1 157 1
+2344 1 158 1
+2345 1 159 1
+2346 2 160 1
+2347 2 161 1
+2348 2 162 1
+2349 1 163 1
+2350 1 164 1
+2351 1 165 1
+2352 2 166 1
+2353 2 168 1
+2354 1 169 1
+2355 1 170 1
+2356 1 171 1
+2357 1 172 1
+2358 1 173 1
+2359 2 0 1
+2360 1 1 1
+2361 1 2 1
+2362 1 3 1
+2363 1 4 1
+2364 1 5 1
+2365 1 6 1
+2366 1 7 1
+2367 0 8 1
+2368 0 9 1
+2369 0 10 1
+2370 1 11 1
+2371 1 12 1
+2372 1 13 1
+2373 1 14 1
+2374 0 15 1
+2375 0 16 1
+2376 0 17 1
+2377 1 18 1
+2378 1 19 1
+2379 1 20 1
+2380 1 22 1
+2381 0 23 1
+2382 0 24 1
+2383 0 25 1
+2384 1 26 1
+2385 1 27 1
+2386 1 201 1
+2387 1 202 1
+2388 1 203 1
+2389 1 204 1
+2390 1 205 1
+2391 1 206 1
+2392 1 207 1
+2393 0 208 1
+2394 0 209 1
+2395 0 210 1
+2396 1 211 1
+2397 1 212 1
+2398 1 213 1
+2399 0 214 1
+2400 0 215 1
+2401 0 216 1
+2402 0 217 1
+2403 0 218 1
+2404 1 219 1
+2405 1 220 1
+2406 1 221 1
+2407 1 222 1
+3010 1 2542 1
+3011 1 2543 1
+3012 1 2544 1
+3013 1 2545 1
+3014 2 2546 1
+3015 2 2547 1
+3016 2 2548 1
+3017 1 2549 1
+3018 1 2550 1
+3019 2 2552 1
+3020 2 2553 1
+3021 2 2554 1
+3022 1 2555 1
+3023 1 2556 1
+3024 1 2558 1
+3025 1 2559 1
+3026 2 2408 1
+3027 1 2409 1
+3028 1 2410 1
+3029 1 2412 1
+3030 1 2413 1
+3031 1 2414 1
+3032 0 2416 1
+3033 0 2417 1
+3034 1 2419 1
+3035 1 2420 1
+3036 1 2421 1
+3037 0 2423 1
+3038 0 2424 1
+3039 1 2426 1
+3040 1 2427 1
+3041 1 2428 1
+3042 1 2429 1
+3043 1 2430 1
+3044 0 2431 1
+3045 0 2432 1
+3046 1 2433 1
+3047 1 2434 1
+3048 1 2560 1
+3049 1 2561 1
+3050 1 2562 1
+3051 1 2563 1
+3052 2 2564 1
+3053 2 2565 1
+3054 2 2566 1
+3055 1 2567 1
+3056 1 2568 1
+3057 2 2570 1
+3058 2 2571 1
+3059 2 2572 1
+3060 1 2573 1
+3061 1 2574 1
+3062 1 2576 1
+3063 1 2577 1
+3064 2 2408 1
+3065 1 2409 1
+3066 1 2410 1
+3067 1 2412 1
+3068 1 2413 1
+3069 1 2414 1
+3070 0 2416 1
+3071 0 2417 1
+3072 1 2419 1
+3073 1 2420 1
+3074 1 2421 1
+3075 0 2423 1
+3076 0 2424 1
+3077 1 2426 1
+3078 1 2427 1
+3079 1 2428 1
+3080 1 2429 1
+3081 1 2430 1
+3082 0 2431 1
+3083 0 2432 1
+3084 1 2433 1
+3085 1 2434 1
+3086 1 2600 1
+3087 1 2601 1
+3088 1 2602 1
+3089 1 2603 1
+3090 1 2604 1
+3091 1 2605 1
+3092 1 2606 1
+3093 0 2607 1
+3094 0 2608 1
+3095 1 2609 1
+3096 1 2610 1
+3097 1 2611 1
+3098 0 2612 1
+3099 0 2613 1
+3100 0 2614 1
+3101 0 2615 1
+3102 1 2616 1
+3103 1 2617 1
+3104 1 2618 1
+3105 1 2619 1
+3150 1 2551 1
+3151 1 2557 1
+3152 1 2411 1
+3153 1 2415 1
+3154 0 2418 1
+3155 1 2422 1
+3156 0 2425 1
+3157 1 2569 1
+3158 1 2575 1
+3159 1 2411 1
+3160 1 2415 1
+3161 0 2418 1
+3162 1 2422 1
+3163 0 2425 1
+3164 0 2620 1
+3165 0 2621 1
+3170 0 2599 1
+3171 0 2599 1