Introduction

Execution Chart

We display below the execution chart for this examination (boot time has been removed).

Sequence of Actions to be Executed by the VM

This is useful if one wants to reexecute the tool in the VM from the submitted image disk.

export BK_INPUT=GlobalRessAlloc-PT-03
export BK_EXAMINATION=CTLPlaceComparison
export BK_TOOL=marcie
export BK_RESULT_DIR=/tmp
export BK_LOG_FILE=/tmp/BenchKit_head_log_file.1655
export BIN_DIR=/home/mcc/BenchKit/bin
cd /home/mcc/BenchKit/INPUTS/GlobalRessAlloc-PT-03
echo =====================================================================
echo ' Generated by BenchKit 1.0'
echo ' Executing tool marcie:'
echo ' Test is GlobalRessAlloc-PT-03, examination is CTLPlaceComparison'
echo =====================================================================
echo
echo --------------------
echo 'content from stdout:'
echo
bash /home/mcc/BenchKit/BenchKit_head.sh

Execution Outputs of marcie for GlobalRessAlloc/03 (P/T)

This is useful if one wants to reexecute the tool in the VM from the submitted image disk.

execution on node 4: quadhexa-2.u-paris10.fr (runId=136952151900080_n_4)
=====================================================================
runnning marcie on GlobalRessAlloc-PT-03 (CTLPlaceComparison)
We got on stdout:
Probing ssh
Waiting ssh to respond
Ssh up and responding
=====================================================================
Generated by BenchKit 1.0
Executing tool marcie:
Test is GlobalRessAlloc-PT-03, examination is CTLPlaceComparison
=====================================================================

--------------------
content from stdout:

START 1369528846

Marcie rev. 1103M (build: rohrch on 2013-02-17)
A model checker for Generalized Stochastic Petri nets

authors: Alex Tovchigrechko (IDD package and CTL model checking)

Martin Schwarick (Symbolic numerical analysis and CSL model checking)

Christian Rohr (Simulative and approximative numerical model checking)

marcie@informatik.tu-cottbus.de

called as: marcie --net-file=model.pnml --mem=4 --mcc-file=CTLPlaceComparison.txt

constant oo registered with value < INFINITY >
parse successfull!


(NrP: 33 NrTr: 4791)

net check time: 0m0sec

parse mcc successfull!

place and transition orderings generation:0m0sec

init dd package: 0m8sec


RS generation: 0m40sec


-> reachability set: #nodes 3060 (3.1e+03) #states 6,320 (3)



starting CTL model checker
--------------------------

checking: EG [[[pr_released_3=pr_in_3 & [pr_released_2=pr_in_2 & [pr_released_1=pr_in_1 & true]]] & [pr_in_1!=pr_released_1 & [pr_in_2!=pr_released_2 & [pr_in_3!=pr_released_3 & true]]]]]
normalized: EG [[[[pr_released_2=pr_in_2 & [true & pr_released_1=pr_in_1]] & pr_released_3=pr_in_3] & [[pr_in_2!=pr_released_2 & [true & pr_in_3!=pr_released_3]] & pr_in_1!=pr_released_1]]]

.
EG iterations: 1
-> the formula is FALSE

FORMULA p_1846_placecomparison_eq_and FALSE TECHNIQUES DECISION_DIAGRAMS

mc time: 0m0sec

checking: AF [[[pr_released_3=pr_in_3 & [pr_released_2=pr_in_2 & [pr_released_1=pr_in_1 & true]]] | [pr_in_1!=pr_released_1 & [pr_in_2!=pr_released_2 & [pr_in_3!=pr_released_3 & true]]]]]
normalized: ~ [EG [~ [[[pr_in_1!=pr_released_1 & [[true & pr_in_3!=pr_released_3] & pr_in_2!=pr_released_2]] | [pr_released_3=pr_in_3 & [[true & pr_released_1=pr_in_1] & pr_released_2=pr_in_2]]]]]]


EG iterations: 0
-> the formula is FALSE

FORMULA p_1847_placecomparison_eq_or FALSE TECHNIQUES DECISION_DIAGRAMS

mc time: 0m0sec

checking: AF [[[pr_released_3=pr_in_3 & [pr_released_2=pr_in_2 & [pr_released_1=pr_in_1 & true]]] & [pr_in_1!=pr_released_1 & [pr_in_2!=pr_released_2 & [pr_in_3!=pr_released_3 & true]]]]]
normalized: ~ [EG [~ [[[pr_in_1!=pr_released_1 & [[true & pr_in_3!=pr_released_3] & pr_in_2!=pr_released_2]] & [pr_released_3=pr_in_3 & [[true & pr_released_1=pr_in_1] & pr_released_2=pr_in_2]]]]]]


EG iterations: 0
-> the formula is FALSE

FORMULA p_1848_placecomparison_eq_and_notx FALSE TECHNIQUES DECISION_DIAGRAMS

mc time: 0m0sec

checking: AG [[[pr_released_3=pr_in_3 & [pr_released_2=pr_in_2 & [pr_released_1=pr_in_1 & true]]] | [pr_in_1!=pr_released_1 & [pr_in_2!=pr_released_2 & [pr_in_3!=pr_released_3 & true]]]]]
normalized: ~ [E [true U ~ [[[pr_in_1!=pr_released_1 & [pr_in_2!=pr_released_2 & [pr_in_3!=pr_released_3 & true]]] | [pr_released_3=pr_in_3 & [pr_released_2=pr_in_2 & [pr_released_1=pr_in_1 & true]]]]]]]

-> the formula is FALSE

FORMULA p_1849_placecomparison_eq_or_notx FALSE TECHNIQUES DECISION_DIAGRAMS

mc time: 0m5sec

checking: EG [AG [[AF [[pr_released_3=pr_in_3 & [pr_released_2=pr_in_2 & [pr_released_1=pr_in_1 & true]]]] | [pr_in_1!=pr_released_1 & [pr_in_2!=pr_released_2 & [pr_in_3!=pr_released_3 & true]]]]]]
normalized: EG [~ [E [true U ~ [[[pr_in_1!=pr_released_1 & [pr_in_2!=pr_released_2 & [pr_in_3!=pr_released_3 & true]]] | ~ [EG [~ [[pr_released_3=pr_in_3 & [pr_released_2=pr_in_2 & [true & pr_released_1=pr_in_1]]]]]]]]]]]


EG iterations: 0
.
EG iterations: 1
-> the formula is FALSE

FORMULA p_1850_placecomparison_eq_x FALSE TECHNIQUES DECISION_DIAGRAMS

mc time: 0m0sec

checking: EF [[[[false | [pr_released_3>pr_in_3 | [pr_released_2>pr_in_2 | [pr_released_1>pr_in_1 | false]]]] & [[pr_released_3>pr_in_3 & [pr_released_2>pr_in_2 & [pr_released_1>pr_in_1 & true]]] & true]] & [[false | [pr_in_1>Processes_1 | [pr_in_2>Processes_2 | [pr_in_3>Processes_3 | false]]]] & [[pr_in_1>Processes_1 & [pr_in_2>Processes_2 & [pr_in_3>Processes_3 & true]]] & true]]]]
normalized: E [true U [[[true & [[[pr_in_3>Processes_3 & true] & pr_in_2>Processes_2] & pr_in_1>Processes_1]] & [[pr_in_1>Processes_1 | [pr_in_2>Processes_2 | [false | pr_in_3>Processes_3]]] | false]] & [[[pr_released_3>pr_in_3 | [pr_released_2>pr_in_2 | [pr_released_1>pr_in_1 | false]]] | false] & [[pr_released_3>pr_in_3 & [pr_released_2>pr_in_2 & [pr_released_1>pr_in_1 & true]]] & true]]]]

-> the formula is FALSE

FORMULA p_1851_placecomparison_full_and FALSE TECHNIQUES DECISION_DIAGRAMS

mc time: 0m0sec

checking: EF [[[[false | [pr_released_3>pr_in_3 | [pr_released_2>pr_in_2 | [pr_released_1>pr_in_1 | false]]]] & [[pr_released_3>pr_in_3 & [pr_released_2>pr_in_2 & [pr_released_1>pr_in_1 & true]]] & true]] | [[false | [pr_in_1>Processes_1 | [pr_in_2>Processes_2 | [pr_in_3>Processes_3 | false]]]] & [[pr_in_1>Processes_1 & [pr_in_2>Processes_2 & [pr_in_3>Processes_3 & true]]] & true]]]]
normalized: E [true U [[[[[[false | pr_released_1>pr_in_1] | pr_released_2>pr_in_2] | pr_released_3>pr_in_3] | false] & [true & [[pr_released_2>pr_in_2 & [pr_released_1>pr_in_1 & true]] & pr_released_3>pr_in_3]]] | [[true & [[[true & pr_in_3>Processes_3] & pr_in_2>Processes_2] & pr_in_1>Processes_1]] & [[pr_in_1>Processes_1 | [[pr_in_3>Processes_3 | false] | pr_in_2>Processes_2]] | false]]]]

-> the formula is FALSE

FORMULA p_1852_placecomparison_full_or FALSE TECHNIQUES DECISION_DIAGRAMS

mc time: 0m0sec

checking: AF [[[[false | [pr_released_3>pr_in_3 | [pr_released_2>pr_in_2 | [pr_released_1>pr_in_1 | false]]]] & [[pr_released_3>pr_in_3 & [pr_released_2>pr_in_2 & [pr_released_1>pr_in_1 & true]]] & true]] & ~ [[[false | [pr_in_1>Processes_1 | [pr_in_2>Processes_2 | [pr_in_3>Processes_3 | false]]]] & [[pr_in_1>Processes_1 & [pr_in_2>Processes_2 & [pr_in_3>Processes_3 & true]]] & true]]]]]
normalized: ~ [EG [~ [[[[[pr_released_3>pr_in_3 | [pr_released_2>pr_in_2 | [pr_released_1>pr_in_1 | false]]] | false] & [[[[true & pr_released_1>pr_in_1] & pr_released_2>pr_in_2] & pr_released_3>pr_in_3] & true]] & ~ [[[[[pr_in_2>Processes_2 | [false | pr_in_3>Processes_3]] | pr_in_1>Processes_1] | false] & [[[pr_in_2>Processes_2 & [pr_in_3>Processes_3 & true]] & pr_in_1>Processes_1] & true]]]]]]]


EG iterations: 0
-> the formula is FALSE

FORMULA p_1853_placecomparison_full_and_notx FALSE TECHNIQUES DECISION_DIAGRAMS

mc time: 0m0sec


total processing time: 1m20sec

STOP 1369528926

--------------------
content from stderr:

check if there are places and transitions
ok
check if there are transitions without pre-places
ok
check if at least one transition is enabled in m0
ok
check if there are transitions that can never fire
ok


initing FirstDep: 0m0sec

133 170 176 207 233 240 247 259 269 274 281 287 291 295 300 318 318 328 328 336 338 351 346 346 354 354 385 390 386 389 388 385 405 403 399 403 410 409 408 409 410 411 408 407 405 403 400 407 414 420 427 445 444 445 447 448 457 458 460 460 464 467 467 467 474 475 485 485 493 493 497 500 501 510 508 508 518 518 522 524 523 522 526 525 529 532 532 540 539 552 552 567 565 577 570 578 578 584 591 591 602 606 612 614 615 616 621 620 625 635 635 640 641 641 649 662 657 657 669 662 664 665 670 672 673 673 679 689 685 685 688 690 691 691 696 697 697 707 707 721 717 717 728 720 724 727 727 733 737 737 746 746 757 752 752 760 760 773 773 766 766 773 789 785 779 779 788 788 803 803 800 797 797 801 801 801 805 805 808 808 814 814 814 818 818 818 818 857 857 857 890 890 896 896 899 899 901 908 903 903 903 942 940 940 938 936 936 934 940 940 946 946 951 954 954 962 962 967 965 965 967 967 976 976 971 975 975 973 973 981 981 981 981 1020 1017 1014 1011 1011 1016 1021 1021 1023 1029 1023 1025 1025 1030 1027 1033 1027 1041 1030 1030 1035 1032 1032 1035 1035 1035 1079 1072 1063 1063 1065 1069 1069 1071 1071 1071 1081 1071 1078 1074 1072 1072 1077 1072 1078 1074 1082 1080 1080 1080 1324 1316 1304 1299 1284 1280 1276 1272 1271 1268 1257 1252 1248 1248 1244 1240 1240 1236 1240 1240 1244 1244 1250 1253 1248 1252 1252 1266 1259 1259 1264 1268 1262 1268 1266 1266 1269 1271 1271 1275 1275 1273 1278 1276 1276 1279 1282 1282 1289 1286 1294 1286 1302 1291 1291 1298 1293 1297 1294 1294 1296 1298 1298 1304 1301 1306 1303 1303 1309 1326 1319 1319 1312 1312 1314 1314 1314 1315 1315 1315 1319 1321 1321 1323 1323 1324 1324 1324 1474 1470 1467 1463 1454 1452 1450 1448 1446 1461 1468 1464 1464 1464 1463 1462 1453 1449 1449 1448 1444 1434 1433 1404 1394 1396 1390 1392 1385 1387 1382 1384 1376 1376 1370 1370 1374 1374 1378 1384 1387 1381 1391 1385 1392 1385 1385 1397 1399 1388 1395 1394 1388 1400 1395 1397 1398 1386 1386 1390 1391 1386 1386 1395 1389 1390 1390 1390 1390 1394 1388 1388 1386 1386 1388 1388 1390 1390 1396 1388 1388 1394 1388 1389 1389 1401 1389 1389 1399 1397 1389 1389 1394 1395 1390 1389 1389 1398 1386 1395 1389 1390 1381 1384 1385 1380 1380 1379 1390 1387 1375 1376 1376 1386 1386 1375 1377 1377 1388 1388 1378 1378 1377 1394 1389 1385 1372 1372 1372 1370 1370 1371 1371 1373 1373 1377 1377 1383 1379 1379 1382 1382 1384 1384 1397 1397 1390 1390 1395 1391 1391 1392 1392 1394 1394 1401 1397 1397 1394 1394 1394 1381 1381 1381 1427 1423 1423 1419 1416 1413 1410 1410 1410 1414 1418 1418 1425 1421 1421 1423 1423 1422 1445 1433 1426 1432 1427 1427 1433 1427 1430 1430 1429 1429 1429 1429 1661 1654 1652 1645 1642 1636 1630 1622 1617 1613 1609 1608 1606 1606 1601 1593 1588 1585 1585 1582 1584 1579 1576 1576 1573 1573 1573 1573 1573 1577 1574 1574 1571 1571 1576 1570 1570 1574 1571 1571 1576 1573 1573 1573 1570 1570 1573 1576 1570 1574 1571 1571 1575 1584 1584 1576 1576 1576 1576 1577 1577 1582 1582 1579 1579 1586 1578 1594 1584 1577 1577 1580 1580 1577 1577 1583 1580 1580 1580 1579 1578 1578 1581 1581 1577 1580 1576 1576 1576 1579 1588 1588 1580 1580 1580 1585 1587 1587 1587 1587 1587 1587 1587 1588 1588 1588 1627 1626 1625 1624 1625 1622 1623 1620 1620 1621 1618 1619 1616 1616 1618 1618 1621 1621 1626 1623 1623 1631 1627 1633 1625 1643 1634 1634 1628 1631 1631 1628 1628 1634 1627 1631 1624 1631 1628 1628 1628 1666 1664 1664 1662 1665 1660 1658 1658 1658 1660 1660 1662 1663 1663 1662 1662 1662 1693 1693 1693 1693 1724 1724 1724 1730 1733 1733 1736 1736 1740 1740 1740 1785 1775 1774 1774 1773 1773 1772 1771 1771 1777 1783 1783 1788 1788 1792 1792 1800 1800 1805 1804 1804 1807 1807 1818 1818 1815 1815 1821 1823 1820 1827 1826 1826 1826 1873 1868 1863 1861 1857 1857 1862 1862 1867 1867 1870 1872 1872 1876 1876 1881 1879 1879 1881 1881 1890 1887 1887 1892 1890 1890 1893 1893 1893 2047 2044 2040 2038 2031 2028 2025 2022 2025 2021 2017 2014 2012 2012 2010 2008 2008 2006 2006 2009 2011 2011 2015 2013 2013 2015 2015 2028 2024 2020 2029 2025 2023 2023 2028 2026 2030 2030 2032 2032 2036 2036 2034 2034 2040 2038 2038 2043 2052 2052 2045 2045 2047 2047 2047 2052 2052 2054 2061 2056 2064 2059 2059 2059 2099 2096 2097 2094 2096 2092 2092 2093 2090 2092 2088 2088 2089 2086 2086 2090 2090 2094 2099 2099 2096 2096 2104 2099 2107 2101 2125 2119 2113 2108 2108 2114 2116 2111 2118 2118 2112 2118 2113 2113 2117 2117 2117 2117 2154 2150 2148 2148 2146 2146 2144 2144 2148 2148 2151 2151 2154 2154 2156 2156 2156 2178 2178 2178 2225 2201 2201 2201 2204 2203 2203 2210 2203 2205 2205 2205 2205 2246 2244 2239 2241 2237 2232 2232 2228 2228 2231 2235 2235 2238 2238 2239 2257 2240 2240 2244 2239 2239 2246 2238 2255 2245 2246 2239 2245 2245 2241 2241 2248 2243 2243 2243 2287 2284 2281 2279 2267 2267 2270 2270 2274 2282 2277 2276 2276 2283 2277 2282 2276 2276 2277 2277 2291 2285 2279 2283 2284 2278 2282 2276 2276 2276 2421 2422 2411 2412 2402 2394 2390 2385 2385 2378 2375 2368 2364 2364 2359 2360 2355 2351 2351 2350 2350 2348 2351 2351 2346 2346 2344 2344 2354 2348 2343 2348 2346 2348 2342 2345 2341 2341 2342 2351 2341 2350 2345 2347 2342 2348 2344 2344 2346 2346 2355 2345 2345 2345 2344 2344 2344 2347 2347 2345 2351 2345 2345 2348 2348 2348 2390 2387 2386 2385 2384 2385 2382 2385 2377 2377 2378 2375 2375 2372 2372 2372 2375 2375 2380 2380 2383 2378 2378 2386 2380 2380 2383 2383 2405 2391 2391 2386 2386 2392 2394 2389 2394 2394 2387 2391 2385 2392 2387 2387 2387 2423 2425 2421 2416 2416 2414 2414 2409 2409 2409 2412 2422 2414 2423 2416 2424 2417 2417 2417 2443 2443 2443 2483 2476 2469 2469 2473 2482 2474 2479 2474 2474 2474 2474 2474 2520 2515 2510 2511 2508 2509 2506 2503 2503 2500 2500 2502 2506 2506 2509 2515 2509 2509 2520 2510 2515 2515 2511 2516 2509 2509 2519 2512 2512 2507 2512 2511 2512 2507 2507 2514 2510 2510 2510 2547 2544 2544 2541 2542 2539 2539 2536 2536 2536 2538 2540 2540 2548 2541 2547 2540 2540 2540 2563 2563 2563 2600 2593 2586 2586 2590 2590 2591 2591 2598 2591 2595 2590 2590 2590 2633 2628 2626 2621 2621 2622 2619 2616 2616 2613 2613 2615 2619 2619 2623 2623 2622 2622 2633 2624 2628 2628 2625 2625 2630 2623 2633 2632 2625 2620 2620 2623 2623 2624 2619 2626 2622 2622 2622 2655 2656 2653 2653 2650 2651 2648 2648 2645 2645 2645 2647 2651 2651 2659 2652 2652 2649 2649 2649 2669 2669 2669 2669 2707 2700 2690 2690 2693 2693 2695 2695 2700 2695 2695 2694 2694 2694 2744 2736 2729 2731 2727 2727 2728 2722 2719 2719 2715 2715 2718 2722 2722 2725 2725 2732 2726 2743 2736 2729 2735 2735 2731 2731 2736 2730 2730 2742 2740 2734 2729 2729 2733 2733 2734 2728 2735 2730 2730 2730 2765 2766 2763 2763 2760 2760 2761 2755 2750 2750 2750 2753 2753 2755 2755 2763 2757 2757 2758 2758 2758 2782 2782 2782 2782 2820 2813 2813 2806 2806 2808 2808 2807 2812 2812 2808 2808 2811 2811 2811 2811 2831 2831 2831 2868 2868 2861 2861 2851 2851 2854 2854 2855 2863 2861 2863 2857 2864 2859 2859 2859 2879 2879 2879 2879 2915 2908 2908 2901 2901 2903 2903 2901 2901 2905 2901 2901 2908 2904 2904 2904 2925 2925 2925 2974 2963 2963 2956 2956 2948 2948 2950 2950 2948 2948 2952 2952 2953 2948 2955 2951 2951 2951 2951 2975 2975 2975 2975 2998 2998 2998 2998 3020 3020 3020 3020 3041 3041 3041 3041 3041 3060 3060 3060 3060 3060
iterations count:1481071 (309), effective:2245 (0)

initing FirstDep: 0m0sec

3060 3060 3060 3060
iterations count:4791 (1), effective:0 (0)
3060 3060 3060 3060
iterations count:4791 (1), effective:0 (0)

--------------------
content from /tmp/BenchKit_head_log_file.1655: