1#! /bin/sh 2# -*- coding: utf-8 -*- 3# Copyright (C) 2017, 2019-2021 Laboratoire de Recherche et 4# Développement de l'Epita (LRDE). 5# 6# This file is part of Spot, a model checking library. 7# 8# Spot is free software; you can redistribute it and/or modify it 9# under the terms of the GNU General Public License as published by 10# the Free Software Foundation; either version 3 of the License, or 11# (at your option) any later version. 12# 13# Spot is distributed in the hope that it will be useful, but WITHOUT 14# ANY WARRANTY; without even the implied warranty of MERCHANTABILITY 15# or FITNESS FOR A PARTICULAR PURPOSE. See the GNU General Public 16# License for more details. 17# 18# You should have received a copy of the GNU General Public License 19# along with this program. If not, see <http://www.gnu.org/licenses/>. 20 21. ./defs || exit 1 22 23set -e 24 25cat >exp <<EOF 26parity 17; 270 1 0 7,8 "INIT"; 288 3 1 2; 292 1 0 11,12; 3012 5 1 2,3; 313 1 0 13,14; 3214 4 1 2,3; 3313 4 1 1,4; 344 1 0 8,15; 3515 3 1 5,6; 366 1 0 8,15; 375 1 0 16,17; 3817 4 1 2; 3916 4 1 5,6; 401 1 0 9,10; 4110 3 1 2,3; 429 3 1 1,5; 4311 5 1 1,4; 447 3 1 1,2; 45parity 13; 460 1 0 1,2 "INIT"; 472 1 1 3; 483 3 0 5,4; 494 2 1 12,3; 5012 2 0 5,4; 515 1 1 6,7; 527 1 0 9,8; 538 3 1 12,3; 549 1 1 11,10; 5510 2 0 9,8; 5611 1 0 9,8; 576 1 0 13,4; 5813 1 1 6,10; 591 1 1 6,3; 60parity 5; 611 1 0 4,5 "INIT"; 625 4 1 1,1; 634 5 1 0,1; 640 1 0 2,3; 653 5 1 1; 662 3 1 0,0; 67EOF 68 69: > out 70for algo in ds sd lar; do 71 ltlsynt --ins=a --outs=b -f 'GFa <-> GFb' --algo=$algo --print-pg >>out 72done 73diff out exp 74 75cat >exp <<EOF 76REALIZABLE 77aag 1 1 0 1 0 782 792 80i0 a 81o0 b 82EOF 83ltlsynt --ins=a --outs=b -f 'GFa <-> GFb' --aiger=isop >out 84diff out exp 85 86cat >exp <<EOF 87REALIZABLE 88aag 1 1 0 1 0 892 902 91i0 a 92o0 b 93EOF 94ltlsynt --ins=a --outs=b -f 'GFa <-> GFb' --aiger=isop+dc >out 95diff out exp 96 97cat >exp <<EOF 98REALIZABLE 99aag 1 1 0 1 0 1002 1012 102i0 a 103o0 b 104EOF 105ltlsynt --ins=a --outs=b -f 'GFa <-> GFb' --aiger=isop+ud >out 106diff out exp 107 108cat >exp <<EOF 109REALIZABLE 110aag 1 1 0 1 0 1112 1122 113i0 a 114o0 b 115EOF 116ltlsynt --ins=a --outs=b -f 'GFa <-> GFb' --aiger=isop+sub1 >out 117diff out exp 118 119cat >exp <<EOF 120REALIZABLE 121aag 1 1 0 1 0 1222 1232 124i0 a 125o0 b 126EOF 127ltlsynt --ins=a --outs=b -f 'GFa <-> GFb' --aiger=isop+sub2 >out 128diff out exp 129 130cat >exp <<EOF 131REALIZABLE 132aag 1 1 0 1 0 1332 1342 135i0 a 136o0 b 137EOF 138ltlsynt --ins=a --outs=b -f 'GFa <-> GFb' --aiger=isop,isop+dc,isop+ud >out 139diff out exp 140ltlsynt --ins=a --outs=b -f 'GFa <-> GFb' --aiger=ite >out 141diff out exp 142ltlsynt --ins=a --outs=b -f 'GFa <-> GFb' --aiger=ite+ud+dc >out 143diff out exp 144ltlsynt --ins=a --outs=b -f 'GFa <-> GFb' --aiger >out 145diff out exp 146 147cat >exp <<EOF 148REALIZABLE 149aag 3 1 1 2 1 1502 1514 1 1526 1536 1546 2 4 155i0 a 156o0 b 157o1 c 158EOF 159ltlsynt --ins=a --outs=b,c -f 'GFa <-> (GFb & GFc)' \ 160 --algo=ds --simplify=no --aiger=isop >out 161diff out exp 162 163cat >exp <<EOF 164REALIZABLE 165aag 2 1 1 2 0 1662 1674 1 1682 1692 170i0 a 171o0 b 172o1 c 173EOF 174ltlsynt --ins=a --outs=b,c -f 'GFa <-> (GFb & GFc)' \ 175 --algo=ds --simplify=no --aiger=isop+dc >out 176diff out exp 177 178cat >exp <<EOF 179REALIZABLE 180aag 3 1 1 2 1 1812 1824 1 1836 1846 1856 4 2 186i0 a 187o0 b 188o1 c 189EOF 190ltlsynt --ins=a --outs=b,c -f 'GFa <-> (GFb & GFc)' \ 191 --algo=ds --simplify=no --aiger=ite >out 192diff out exp 193 194cat >exp <<EOF 195trying to create strategy directly for GFa <-> GFb 196tanslating formula done in X seconds 197direct strategy was found. 198direct strat has 1 states and 0 colors 199EOF 200ltlsynt --ins='a' --outs='b' -f 'GFa <-> GFb' --verbose --realizability 2> out 201sed 's/ [0-9.e-]* seconds/ X seconds/g' out > outx 202diff outx exp 203 204cat >exp <<EOF 205trying to create strategy directly for GFa <-> GFb 206tanslating formula done in X seconds 207direct strategy was found. 208direct strat has 1 states and 0 colors 209final strategy has 1 states and 2 edges 210minimization took X seconds 211EOF 212ltlsynt --ins=a --outs=b -f 'GFa <-> GFb' --verbose --algo=ps 2> out 213sed 's/ [0-9.e-]* seconds/ X seconds/g' out > outx 214diff outx exp 215 216cat >exp <<EOF 217trying to create strategy directly for (Fa & Fb & Fc & Fd) <-> GFe 218tanslating formula done in X seconds 219direct strategy was found. 220direct strat has 16 states and 0 colors 221EOF 222ltlsynt --ins='a,b,c,d' --outs='e' -f '(Fa & Fb & Fc & Fd) <-> GFe' \ 223 --verbose --realizability --algo=lar 2> out 224sed 's/ [0-9.e-]* seconds/ X seconds/g' out > outx 225diff outx exp 226 227cat >exp <<EOF 228trying to create strategy directly for G(Fi0 & Fi1 & Fi2) -> G(i1 <-> o0) 229direct strategy might exist but was not found. 230translating formula done in X seconds 231automaton has 2 states and 3 colors 232LAR construction done in X seconds 233DPA has 4 states, 3 colors 234split inputs and outputs done in X seconds 235automaton has 12 states 236solving game with acceptance: parity max odd 5 237game solved in X seconds 238EOF 239ltlsynt -f "G(Fi0 && Fi1 && Fi2) -> G(i1 <-> o0)" --outs="o0" --algo=lar \ 240 --verbose --realizability 2> out 241sed 's/ [0-9.e-]* seconds/ X seconds/g' out > outx 242diff outx exp 243 244 245for r in '' '--real'; do 246 opts="$r --ins=a,c --outs=b -f" 247 ltlsynt --algo=ds $opts 'GFa <-> GFb' --csv=FILE || : 248 ltlsynt --algo=sd $opts 'FGa <-> GF(b&XXb)' --csv='>>FILE' || : 249 ltlsynt --algo=ps $opts 'FGa <-> GF(b&XXb)' --csv='>>FILE' || : 250 ltlsynt --algo=lar $opts 'FGc <-> GF(!b&XXb)' --csv='>>FILE' || : 251 ltlsynt --algo=lar.old $opts 'FGa <-> GF(c&a)' --csv='>>FILE' || : 252 test 6 = `wc -l < FILE` 253 # Make sure all lines in FILE have the same number of commas 254 sed 's/[^,]//g' < FILE | 255 ( read first 256 while read l; do 257 test "x$first" = "x$l" || exit 1 258 done) 259done 260for a in sd ds lar lar.old; do 261 test 1 = `grep -c ",.$a.," FILE` || exit 1 262done 263 264# ltlsynt --algo=lar --ins=a --outs=b -f 'FGa <-> GF(c&a)' --print-pg --csv >out 265# grep parity out 266# grep 'FGa.*,"lar",' out 267# grep formula out 268 269 270F0='(G ((((req) -> (X ((grant) && (X ((grant) && (X (grant))))))) && ((grant) 271-> (X (! (grant))))) && ((cancel) -> (X ((! (grant)) U (go))))))' 272IN0='cancel, go, req' 273OUT0='grant' 274EXP0='UNREALIZABLE' 275F1='(G ((((req) -> (X ((grant) || (X ((grant) || (X (grant))))))) && ((grant) 276-> (X (! (grant))))) && ((cancel) -> (X ((! (grant)) U (go))))))' 277IN1='cancel, go, req' 278OUT1='grant' 279EXP1='UNREALIZABLE' 280F2='((G ((cancel) -> (X (go)))) -> (G ((((req) -> (X ((grant) || (X ((grant) || 281(X (grant))))))) && ((grant) -> (X (! (grant))))) && ((cancel) -> (X ((! 282(grant)) U (go)))))))' 283IN2='cancel, go, req' 284OUT2='grant' 285EXP2='REALIZABLE' 286F3='((G ((cancel) -> (X ((go) || (X (go)))))) -> (G ((((req) -> (X ((grant) || 287(X ((grant) || (X (grant))))))) && ((grant) -> (X (! (grant))))) && ((cancel) 288-> (X ((! (grant)) U (go)))))))' 289IN3='cancel, go, req' 290OUT3='grant' 291EXP3='REALIZABLE' 292F4='((G ((cancel) -> (X ((go) || (X (go)))))) -> (G ((((req) -> (X (((grant) || 293(cancel)) || (X (((grant) || (cancel)) || (X ((grant) || (cancel)))))))) && 294((grant) -> (X (! (grant))))) && ((cancel) -> (X ((! (grant)) U (go)))))))' 295IN4='cancel, go, req' 296OUT4='grant' 297EXP4='REALIZABLE' 298F5='((G ((cancel) -> (X ((go) || (X ((go) || (X (go)))))))) -> (G ((((req) -> 299(X (((grant) || (cancel)) || (X (((grant) || (cancel)) || (X ((grant) || 300(cancel)))))))) && ((grant) -> (X (! (grant))))) && ((cancel) -> (X ((! 301(grant)) U (go)))))))' 302IN5='cancel, go, req' 303OUT5='grant' 304EXP5='REALIZABLE' 305F6='((G ((cancel) -> (X ((go) || (X (go)))))) -> (G ((((cancel) -> (X ((! 306(grant)) U (go)))) && ((grant) -> (X (! (grant))))) && ((req) -> (((grant) || 307(cancel)) || (X (((grant) || (cancel)) || (X (((grant) || (cancel)) || (X 308((grant) || (cancel))))))))))))' 309IN6='cancel, go, req' 310OUT6='grant' 311EXP6='REALIZABLE' 312F7='(! ((G ((req) -> (F (ack)))) && (G ((go) -> (F (grant))))))' 313IN7='go, req' 314OUT7='ack, grant' 315EXP7='UNREALIZABLE' 316F8='(((G ((((r1) -> (F (a1))) && ((r2) -> (F (a2)))) && (! ((a1) && (a2))))) && 317(((a1) U (r1)) || (G (a1)))) && (((a2) U (r2)) || (G (a2))))' 318IN8='r1, r2' 319OUT8='a1, a2' 320EXP8='UNREALIZABLE' 321F9='((((G (((((((r0) -> (F (a0))) && ((r1) -> (F (a1)))) && ((r2) -> (F (a2)))) 322&& (! ((a0) && (a1)))) && (! ((a0) && (a2)))) && (! ((a1) && (a2))))) && (((a0) 323U (r0)) || (G (a0)))) && (((a1) U (r1)) || (G (a1)))) && (((a2) U (r2)) || (G 324(a2))))' 325IN9='r0, r1, r2' 326OUT9='a0, a1, a2' 327EXP9='UNREALIZABLE' 328IN10='a, b, c' 329OUT10='p0, p1, p2' 330F10='G (p0 && ! p1 && ! p2 || (! p0 && p1 && ! p2) || (! p0 && ! p1 && p2)) && 331 (F (G a) || F (G b) || G (F c) <-> (G (F p0) || (G (F p1) && ! G (F p2))))' 332EXP10='REALIZABLE' 333 334for i in 0 1 7 8 9; do 335 F=$(eval echo \$F$i) 336 IN=$(eval echo \$IN$i) 337 OUT=$(eval echo \$OUT$i) 338 EXP=$(eval echo \$EXP$i) 339 340 for algo in sd ds lar; do 341 test $EXP = $(ltlsynt -f "$F" --ins="$IN" --outs="$OUT" --realizability \ 342 --algo=$algo) 343 done 344done 345 346for i in 2 3 4 5 6 10; do 347 F=$(eval echo \$F$i) 348 IN=$(eval echo \$IN$i) 349 OUT=$(eval echo \$OUT$i) 350 EXP=$(eval echo \$EXP$i) 351 352 ltl2tgba -f "!($F)" > negf_aut$i 353 354 # test ltlsynt 355 for algo in sd ds ps lar lar.old; do 356 ltlsynt -f "$F" --ins="$IN" --outs="$OUT" --algo=$algo > out$i || true 357 REAL=`head -1 out$i` 358 test $REAL = $EXP 359 tail -n +2 out$i > res$i 360 # check that the L(strategy) is included in L(F) 361 autfilt -q -v --intersect=negf_aut$i res$i 362 # check that all environment actions are possible 363 autfilt --remove-ap="$OUT" res$i | autfilt --dualize | autfilt --is-empty -q 364 done 365done 366 367cat >exp <<EOF 368REALIZABLE 369HOA: v1 370States: 3 371Start: 0 372AP: 1 "p0" 373acc-name: all 374Acceptance: 0 t 375properties: trans-labels explicit-labels state-acc deterministic 376--BODY-- 377State: 0 378[t] 1 379State: 1 380[t] 2 381State: 2 382[!0] 2 383--END-- 384EOF 385ltlsynt --outs=p0 -x tls-impl=0 --simpl=no -f '!XXF(p0 & (p0 M Gp0))' > out 386diff out exp 387 388cat >exp <<EOF 389REALIZABLE 390HOA: v1 391States: 1 392Start: 0 393AP: 1 "p0" 394acc-name: all 395Acceptance: 0 t 396properties: trans-labels explicit-labels state-acc deterministic 397--BODY-- 398State: 0 399[!0] 0 400--END-- 401EOF 402ltlsynt --outs=p0 -x tls-impl=1 -f '!XXF(p0 & (p0 M Gp0))' > out 403diff out exp 404 405ltlsynt --outs=p0 -f '!XXF(p0 & (p0 M Gp0))' > out 406diff out exp 407 408f='Fp0 U XX((p0 & F!p1) | (!p0 & Gp1))' 409ltlsynt --verbose --algo=ps --outs p1 --ins p0 -f "$f" -x"dpa-simul=1" 2>err 410grep 'DPA has 13 states' err 411ltlsynt -x dpa-simul=0 --verbose --algo=ps --outs=p1 --ins=p0 -f "$f" 2>err 412grep 'DPA has 29 states' err 413ltlsynt --verbose -x wdba-minimize=1 --algo=ps --outs=p1 --ins=p0 -f "$f" 2>err 414grep 'DPA has 12 states' err 415 416ltlsynt --outs=p1 -f "$f" -x"dpa-simul=1" --simpl=no | grep 'States: 5' 417ltlsynt --outs=p1 -f "$f" -x"dpa-simul=1" --simpl=bisim | grep 'States: 5' 418ltlsynt --outs=p1 -f "$f" -x"dpa-simul=1" --simpl=bwoa | grep 'States: 4' 419ltlsynt --outs=p1 -f "$f" -x"dpa-simul=1" | grep 'States: 4' 420ltlsynt --outs=p1 -f "$f" -x"dpa-simul=1" --simpl=sat | grep 'States: 2' 421ltlsynt --outs=p1 -f "$f" -x"dpa-simul=1" --simpl=bisim-sat | grep 'States: 2' 422ltlsynt --outs=p1 -f "$f" -x"dpa-simul=1" --simpl=bwoa-sat | grep 'States: 4' 423 424# The following used to raise an exception because of a bug in 425# split_2step_fast_here(). 426for i in 0 1 2 3 4 5; do 427 ltlsynt --ins=a -f 'GFa <-> GFb' --simplify=$i | grep 'States: 1' 428done 429 430cat >exp <<EOF 431REALIZABLE 432aag 34 4 3 2 27 4332 4344 4356 4368 43710 39 43812 62 43914 68 44025 44131 44216 11 13 44318 14 16 44420 10 12 44522 15 20 44624 19 23 44726 11 12 44828 15 26 44930 19 29 45032 7 9 45134 16 32 45236 15 32 45338 35 37 45440 3 32 45542 2 4 45644 6 42 45746 8 42 45848 5 32 45950 10 14 46052 12 14 46154 41 45 46256 47 49 46358 51 53 46460 54 56 46562 58 60 46664 33 51 46766 42 53 46868 64 66 469i0 i0 470i1 i1 471i2 i2 472i3 i3 473o0 o0 474o1 o1 475EOF 476ltlsynt -f "G((i0 && i1)<->X(o0)) && G((i2|i3)<->X(o1))" --outs="o0,o1"\ 477 --aiger=isop --algo=lar --decompose=no --simpl=no >out 478diff out exp 479 480cat >exp <<EOF 481REALIZABLE 482aag 18 4 4 2 10 4832 4844 4856 4868 48710 26 48812 28 48914 34 49016 36 49118 49220 49318 11 12 49420 15 16 49522 2 4 49624 10 12 49726 23 25 49828 22 25 49930 14 16 50032 7 9 50134 31 32 50236 31 33 503i0 i0 504i1 i1 505i2 i2 506i3 i3 507o0 o0 508o1 o1 509EOF 510ltlsynt -f "G((i0 && i1)<->X(o0)) && G((i2|i3)<->X(o1))" --outs="o0,o1"\ 511 --aiger=isop --algo=lar --decompose=yes --simpl=no >out 512diff out exp 513ltlsynt -f "G((i0 && i1)<->X(o0)) && G((i2|i3)<->X(o1))" --outs="o0,o1"\ 514 --aiger=isop --algo=lar --simpl=no >out 515diff out exp 516 517# Issue #477 518ltlsynt -f 'a U (b' 2>err && exit 1 519test $? -eq 2 520test `wc -l <err` -eq 4 521 522 523cat >expected <<EOF 524REALIZABLE 525HOA: v1 526States: 1 527Start: 0 528AP: 3 "a" "b" "c" 529acc-name: all 530Acceptance: 0 t 531properties: trans-labels explicit-labels state-acc deterministic 532--BODY-- 533State: 0 534[!0&!2 | !1&!2] 0 535[0&1&2] 0 536--END-- 537EOF 538ltlsynt --ins=a,b -f 'G (a & b <=> c)' >stdout 539diff stdout expected 540ltlsynt --outs=c -f 'G (a & b <=> c)' >stdout 541diff stdout expected 542 543 544ltlsynt --ins=a,b --outs=c,a -f 'GFa | FGc | GFb' 2>stderr && : 545test $? -eq 2 546grep "'a' appears both" stderr 547 548ltlsynt --ins=a --outs=c -f 'GFa | FGb | GFc' 2>stderr && : 549test $? -eq 2 550grep "both.*but 'b' is unlisted" stderr 551ltlsynt -f 'GFa | FGb | GFc' 2>stderr && : 552test $? -eq 2 553grep "one of --ins or --outs" stderr 554 555# Try to find a direct strategy for GFa <-> GFb and a direct strategy for 556# Gc 557cat >exp <<EOF 558trying to create strategy directly for GFa <-> GFb 559tanslating formula done in X seconds 560direct strategy was found. 561direct strat has 1 states and 0 colors 562final strategy has 1 states and 2 edges 563minimization took X seconds 564trying to create strategy directly for Gc 565direct strategy might exist but was not found. 566translating formula done in X seconds 567automaton has 1 states and 1 colors 568LAR construction done in X seconds 569DPA has 1 states, 2 colors 570split inputs and outputs done in X seconds 571automaton has 2 states 572solving game with acceptance: parity max odd 4 573game solved in X seconds 574EOF 575ltlsynt -f '(GFa <-> GFb) && (Gc)' --outs=b,c --verbose 2> out 576sed 's/ [0-9.e-]* seconds/ X seconds/g' out > outx 577diff outx exp 578 579# Try to find a direct strategy for (GFa <-> GFb) & Gc. THe order should not 580# impact the result 581for f in "(GFa <-> GFb) & Gc" "(GFb <-> GFa) & Gc" \ 582 "Gc & (GFa <-> GFb)" "Gc & (GFb <-> GFa)" 583do 584cat >exp <<EOF 585trying to create strategy directly for $f 586tanslating formula done in X seconds 587direct strategy was found. 588direct strat has 1 states and 0 colors 589final strategy has 1 states and 2 edges 590minimization took X seconds 591EOF 592 ltlsynt -f "$f" --outs=b,c --verbose --decompose=0 --verify 2> out 593 sed 's/ [0-9.e-]* seconds/ X seconds/g' out > outx 594 diff outx exp 595done 596 597# # Ltlsynt should be able to detect that G(a&c) is not input-complete so it is 598# # impossible to find a strategy. 599cat >exp <<EOF 600trying to create strategy directly for (GFb <-> GFa) & G(a & c) 601tanslating formula done in X seconds 602no strategy exists. 603EOF 604ltlsynt -f '(GFb <-> GFa) && G(a&c)' --outs=b,c --verbose\ 605 --decompose=0 2> out || true 606sed 's/ [0-9.e-]* seconds/ X seconds/g' out > outx 607diff outx exp 608 609# # Ltlsynt should be able to create a strategy when the last G 610# is input-complete. 611cat >exp <<EOF 612trying to create strategy directly for (GFb <-> GFa) & G((a & c) | (!a & !c)) 613tanslating formula done in X seconds 614direct strategy was found. 615direct strat has 1 states and 0 colors 616final strategy has 1 states and 2 edges 617minimization took X seconds 618EOF 619ltlsynt -f '(GFb <-> GFa) && (G((a&c)|(!a&!c)))' --outs=b,c --verbose\ 620 --verify --decompose=0 2> out 621sed 's/ [0-9.e-]* seconds/ X seconds/g' out > outx 622diff outx exp 623 624# Direct strategy for persistence 625 626cat >exp <<EOF 627trying to create strategy directly for Fa <-> FGb 628tanslating formula done in X seconds 629direct strategy was found. 630direct strat has 2 states and 0 colors 631final strategy has 2 states and 3 edges 632minimization took X seconds 633EOF 634ltlsynt -f "Fa <-> FGb" --outs=b,c --verbose --decompose=0 --verify 2> out 635sed 's/ [0-9.e-]* seconds/ X seconds/g' out > outx 636diff outx exp 637 638# Test verbose aiger 639 640cat >exp <<EOF 641trying to create strategy directly for Ga <-> Gb 642direct strategy might exist but was not found. 643translating formula done in X seconds 644automaton has 4 states and 1 colors 645LAR construction done in X seconds 646DPA has 4 states, 4 colors 647split inputs and outputs done in X seconds 648automaton has 9 states 649solving game with acceptance: parity max odd 6 650game solved in X seconds 651AIG circuit was created in X seconds and has 0 latches and 0 gates 652EOF 653ltlsynt -f "Ga <-> Gb" --outs=b --verbose --decompose=0 --verify --aiger 2> out 654sed 's/ [0-9.e-]* seconds/ X seconds/g' out > outx 655diff outx exp 656 657cat >exp <<EOF 658trying to create strategy directly for (b & (b | y)) -> y 659direct strategy might exist but was not found. 660translating formula done in X seconds 661automaton has 2 states and 1 colors 662LAR construction done in X seconds 663DPA has 2 states, 2 colors 664split inputs and outputs done in X seconds 665automaton has 4 states 666solving game with acceptance: parity max odd 4 667game solved in X seconds 668trying to create strategy directly for (a | x) -> x 669direct strategy might exist but was not found. 670translating formula done in X seconds 671automaton has 2 states and 1 colors 672LAR construction done in X seconds 673DPA has 2 states, 2 colors 674split inputs and outputs done in X seconds 675automaton has 4 states 676solving game with acceptance: parity max odd 4 677game solved in X seconds 678AIG circuit was created in X seconds and has 0 latches and 0 gates 679EOF 680ltlsynt -f '((a|x) & (b | y) & b) => (x & y)' --outs="x,y" --aiger=ite\ 681 --verify --verbose 2> out 682sed 's/ [0-9.e-]* seconds/ X seconds/g' out > outx 683diff outx exp 684 685# Here, G!(!x | !y) should be Gx & Gy 686cat >exp <<EOF 687trying to create strategy directly for Gx 688direct strategy might exist but was not found. 689translating formula done in X seconds 690automaton has 1 states and 1 colors 691LAR construction done in X seconds 692DPA has 1 states, 2 colors 693split inputs and outputs done in X seconds 694automaton has 2 states 695solving game with acceptance: parity max odd 4 696game solved in X seconds 697trying to create strategy directly for Gy 698direct strategy might exist but was not found. 699translating formula done in X seconds 700automaton has 1 states and 1 colors 701LAR construction done in X seconds 702DPA has 1 states, 2 colors 703split inputs and outputs done in X seconds 704automaton has 2 states 705solving game with acceptance: parity max odd 4 706game solved in X seconds 707AIG circuit was created in X seconds and has 0 latches and 0 gates 708EOF 709ltlsynt -f 'G!(!x | !y)' --outs="x, y" --aiger=ite --verify --verbose 2> out 710sed 's/ [0-9.e-]* seconds/ X seconds/g' out > outx 711diff outx exp 712 713# Here, !F(a | b) should be G(!a) & G(!b) 714cat >exp <<EOF 715trying to create strategy directly for G!a 716direct strategy might exist but was not found. 717translating formula done in X seconds 718automaton has 1 states and 1 colors 719LAR construction done in X seconds 720DPA has 1 states, 2 colors 721split inputs and outputs done in X seconds 722automaton has 4 states 723solving game with acceptance: parity max odd 4 724game solved in X seconds 725EOF 726ltlsynt -f '!F(a|b)' --outs=b --decompose=yes --aiger --verbose 2> out || true 727sed 's/ [0-9.e-]* seconds/ X seconds/g' out > outx 728diff outx exp 729 730# Here, G!(a -> b) should be G(a) & G(!b) 731cat >exp <<EOF 732trying to create strategy directly for Ga 733direct strategy might exist but was not found. 734translating formula done in X seconds 735automaton has 1 states and 1 colors 736LAR construction done in X seconds 737DPA has 1 states, 2 colors 738split inputs and outputs done in X seconds 739automaton has 4 states 740solving game with acceptance: parity max odd 4 741game solved in X seconds 742EOF 743ltlsynt -f 'G!(a -> b)' --outs=b --decompose=yes --aiger\ 744 --verbose 2> out || true 745sed 's/ [0-9.e-]* seconds/ X seconds/g' out > outx 746diff outx exp 747 748# Here, (a & b) U (b & c) should be (a U (b & c)) & (b U (b & c)) 749cat >exp <<EOF 750trying to create strategy directly for (a & b) U (b & c) 751direct strategy might exist but was not found. 752translating formula done in X seconds 753automaton has 2 states and 1 colors 754LAR construction done in X seconds 755DPA has 2 states, 4 colors 756split inputs and outputs done in X seconds 757automaton has 5 states 758solving game with acceptance: parity max odd 6 759game solved in X seconds 760AIG circuit was created in X seconds and has 0 latches and 0 gates 761EOF 762ltlsynt -f '(a & b) U (b & c)' --outs=b,c --decompose=yes --aiger --verbose\ 763 --verify 2> out 764sed 's/ [0-9.e-]* seconds/ X seconds/g' out > outx 765diff outx exp 766 767# Here, a => (b & c & d) should be 768# (a => b) & (a => c) & (a => d) 769cat >exp <<EOF 770trying to create strategy directly for a -> b 771direct strategy might exist but was not found. 772translating formula done in X seconds 773automaton has 2 states and 1 colors 774LAR construction done in X seconds 775DPA has 2 states, 2 colors 776split inputs and outputs done in X seconds 777automaton has 4 states 778solving game with acceptance: parity max odd 4 779game solved in X seconds 780trying to create strategy directly for a -> c 781direct strategy might exist but was not found. 782translating formula done in X seconds 783automaton has 2 states and 1 colors 784LAR construction done in X seconds 785DPA has 2 states, 2 colors 786split inputs and outputs done in X seconds 787automaton has 4 states 788solving game with acceptance: parity max odd 4 789game solved in X seconds 790trying to create strategy directly for a -> d 791direct strategy might exist but was not found. 792translating formula done in X seconds 793automaton has 2 states and 1 colors 794LAR construction done in X seconds 795DPA has 2 states, 2 colors 796split inputs and outputs done in X seconds 797automaton has 4 states 798solving game with acceptance: parity max odd 4 799game solved in X seconds 800AIG circuit was created in X seconds and has 0 latches and 0 gates 801EOF 802ltlsynt -f 'a => (b & c & d)' --outs=b,c,d, --decompose=yes\ 803 --verbose --aiger 2> out 804sed 's/ [0-9.e-]* seconds/ X seconds/g' out > outx 805diff outx exp 806 807# Here, !(F(a | b)) should be G!a & G!b 808cat >exp <<EOF 809trying to create strategy directly for G!a 810direct strategy might exist but was not found. 811translating formula done in X seconds 812automaton has 1 states and 1 colors 813LAR construction done in X seconds 814DPA has 1 states, 2 colors 815split inputs and outputs done in X seconds 816automaton has 4 states 817solving game with acceptance: parity max odd 4 818game solved in X seconds 819EOF 820ltlsynt -f '!(F(a | b))' --outs=b, --decompose=yes \ 821 --verbose --aiger 2> out || true 822sed 's/ [0-9.e-]* seconds/ X seconds/g' out > outx 823diff outx exp 824