1#!/bin/sh 2# -*- coding: utf-8 -*- 3# Copyright (C) 2010, 2011, 2012, 2013, 2014, 2015, 2016 Laboratoire 4# de Recherche et 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 22. ./defs 23 24set -e 25 26# This only runs various configuration of the translation algorithms 27# through valgrind, and checks for differences in the size of the 28# resulting automata. The actual language of the automata is not 29# tested. The columns in the following table are: 30# ltl2tgba options | states | transitions | acc states 31cat >checkta.txt <<\EOF 32in: a 33-TGTA | 4 | 8 | XXX 34-TGTA -RT | 2 | 3 | XXX 35-TA | 3 | 3 | 3 36-TA -RT | 2 | 2 | 2 37-TA -lv | 3 | 3 | 2 38-TA -lv -RT | 2 | 2 | 1 39-TA -sp | 3 | 3 | 2 40-TA -sp -RT | 2 | 2 | 1 41-TA -lv -sp | 3 | 3 | 2 42-TA -lv -sp -RT | 2 | 2 | 1 43-TA -DS | 3 | 3 | 3 44-TA -DS -RT | 2 | 2 | 2 45-TA -DS -lv | 3 | 3 | 3 46-TA -DS -lv -RT | 2 | 2 | 2 47-TA -DS -sp | 3 | 3 | 3 48-TA -DS -sp -RT | 2 | 2 | 2 49-TA -DS -lv -sp | 3 | 3 | 3 50-TA -DS -lv -sp -RT | 2 | 2 | 2 51-x -TA -DS -in | 3 | 3 | 3 52-x -TA -DS -in -RT | 2 | 2 | 2 53in: a U b 54-TGTA | 8 | 34 | XXX 55-TGTA -RT | 4 | 18 | XXX 56-TA | 7 | 20 | 6 57-TA -RT | 4 | 11 | 3 58-TA -lv | 8 | 22 | 5 59-TA -lv -RT | 5 | 13 | 2 60-TA -sp | 7 | 22 | 4 61-TA -sp -RT | 4 | 13 | 1 62-TA -lv -sp | 8 | 22 | 5 63-TA -lv -sp -RT | 5 | 13 | 2 64-TA -DS | 7 | 20 | 6 65-TA -DS -RT | 4 | 11 | 3 66-TA -DS -lv | 8 | 22 | 5 67-TA -DS -lv -RT | 5 | 13 | 2 68-TA -DS -sp | 7 | 22 | 4 69-TA -DS -sp -RT | 4 | 13 | 1 70-TA -DS -lv -sp | 8 | 22 | 5 71-TA -DS -lv -sp -RT | 5 | 13 | 2 72-x -TA -DS -in | 8 | 22 | 5 73-x -TA -DS -in -RT | 5 | 13 | 2 74in: F a 75-TGTA | 5 | 12 | XXX 76-TGTA -RT | 4 | 10 | XXX 77-TA | 4 | 4 | 3 78-TA -RT | 3 | 3 | 2 79-TA -lv | 5 | 5 | 3 80-TA -lv -RT | 4 | 4 | 2 81-TA -sp | 4 | 5 | 2 82-TA -sp -RT | 3 | 4 | 1 83-TA -lv -sp | 5 | 5 | 3 84-TA -lv -sp -RT | 4 | 4 | 2 85-TA -DS | 4 | 4 | 3 86-TA -DS -RT | 3 | 3 | 2 87-TA -DS -lv | 5 | 5 | 3 88-TA -DS -lv -RT | 4 | 4 | 2 89-TA -DS -sp | 4 | 5 | 2 90-TA -DS -sp -RT | 3 | 4 | 1 91-TA -DS -lv -sp | 5 | 5 | 3 92-TA -DS -lv -sp -RT | 4 | 4 | 2 93-x -TA -DS -in | 5 | 5 | 3 94-x -TA -DS -in -RT | 4 | 4 | 2 95in: a & b & c 96-TGTA | 10 | 74 | XXX 97-TGTA -RT | 2 | 9 | XXX 98-TA | 9 | 63 | 9 99-TA -RT | 2 | 14 | 2 100-TA -lv | 9 | 63 | 8 101-TA -lv -RT | 2 | 14 | 1 102-TA -sp | 9 | 63 | 8 103-TA -sp -RT | 2 | 14 | 1 104-TA -lv -sp | 9 | 63 | 8 105-TA -lv -sp -RT | 2 | 14 | 1 106-TA -DS | 9 | 63 | 9 107-TA -DS -RT | 2 | 14 | 2 108-TA -DS -lv | 9 | 63 | 9 109-TA -DS -lv -RT | 2 | 14 | 2 110-TA -DS -sp | 9 | 63 | 9 111-TA -DS -sp -RT | 2 | 14 | 2 112-TA -DS -lv -sp | 9 | 63 | 9 113-TA -DS -lv -sp -RT | 2 | 14 | 2 114-x -TA -DS -in | 9 | 63 | 9 115-x -TA -DS -in -RT | 2 | 14 | 2 116in: a | b | (c U (d & (g U (h ^ i)))) 117-TGTA | 431 | 57396 | XXX 118-TGTA -RT | 10 | 1445 | XXX 119-TA | 430 | 51816 | 328 120-TA -RT | 126 | 15351 | 105 121-TA -lv | 431 | 56744 | 129 122-TA -lv -RT | 128 | 16342 | 2 123-TA -sp | 430 | 56744 | 128 124-TA -sp -RT | 127 | 16342 | 1 125-TA -lv -sp | 431 | 56744 | 129 126-TA -lv -sp -RT | 128 | 16342 | 2 127-TA -DS | 430 | 51816 | 328 128-TA -DS -RT | 127 | 15478 | 106 129-TA -DS -lv | 431 | 56744 | 129 130-TA -DS -lv -RT | 128 | 16342 | 2 131-TA -DS -sp | 430 | 56744 | 128 132-TA -DS -sp -RT | 127 | 16342 | 1 133-TA -DS -lv -sp | 431 | 56744 | 129 134-TA -DS -lv -sp -RT | 128 | 16342 | 2 135-x -TA -DS -in | 431 | 56744 | 129 136-x -TA -DS -in -RT | 128 | 16342 | 2 137in: a & (b U !a) & (b U !a) 138-TGTA | 8 | 30 | XXX 139-TGTA -RT | 4 | 14 | XXX 140-TA | 7 | 20 | 6 141-TA -RT | 2 | 5 | 1 142-TA -lv | 8 | 22 | 5 143-TA -lv -RT | 4 | 10 | 2 144-TA -sp | 7 | 22 | 4 145-TA -sp -RT | 3 | 10 | 1 146-TA -lv -sp | 8 | 22 | 5 147-TA -lv -sp -RT | 4 | 10 | 2 148-TA -DS | 7 | 20 | 6 149-TA -DS -RT | 3 | 8 | 2 150-TA -DS -lv | 8 | 22 | 5 151-TA -DS -lv -RT | 4 | 10 | 2 152-TA -DS -sp | 7 | 22 | 4 153-TA -DS -sp -RT | 3 | 10 | 1 154-TA -DS -lv -sp | 8 | 22 | 5 155-TA -DS -lv -sp -RT | 4 | 10 | 2 156-x -TA -DS -in | 8 | 22 | 5 157-x -TA -DS -in -RT | 4 | 10 | 2 158in: Fa & b & GFc & Gd 159-TGTA | 21 | 219 | XXX 160-TGTA -RT | 7 | 71 | XXX 161-TA | 20 | 182 | 7 162-TA -RT | 10 | 98 | 3 163-TA -lv | 21 | 203 | 5 164-TA -lv -RT | 11 | 112 | 2 165-TA -sp | 20 | 194 | 4 166-TA -sp -RT | 10 | 106 | 1 167-TA -lv -sp | 21 | 203 | 5 168-TA -lv -sp -RT | 11 | 112 | 2 169-TA -DS | 28 | 294 | 15 170-TA -DS -RT | 12 | 126 | 5 171-TA -DS -lv | 29 | 315 | 13 172-TA -DS -lv -RT | 13 | 140 | 4 173-TA -DS -sp | 28 | 306 | 12 174-TA -DS -sp -RT | 12 | 134 | 3 175-TA -DS -lv -sp | 29 | 315 | 13 176-TA -DS -lv -sp -RT | 13 | 140 | 4 177-x -TA -DS -in | 29 | 240 | 9 178-x -TA -DS -in -RT | 12 | 93 | 3 179in: Fa & a & GFc & Gc 180-TGTA | 4 | 8 | XXX 181-TGTA -RT | 3 | 6 | XXX 182-TA | 3 | 3 | 3 183-TA -RT | 2 | 2 | 2 184-TA -lv | 3 | 3 | 2 185-TA -lv -RT | 2 | 2 | 1 186-TA -sp | 3 | 3 | 2 187-TA -sp -RT | 2 | 2 | 1 188-TA -lv -sp | 3 | 3 | 2 189-TA -lv -sp -RT | 2 | 2 | 1 190-TA -DS | 3 | 3 | 3 191-TA -DS -RT | 2 | 2 | 2 192-TA -DS -lv | 3 | 3 | 2 193-TA -DS -lv -RT | 2 | 2 | 1 194-TA -DS -sp | 3 | 3 | 2 195-TA -DS -sp -RT | 2 | 2 | 1 196-TA -DS -lv -sp | 3 | 3 | 2 197-TA -DS -lv -sp -RT | 2 | 2 | 1 198-x -TA -DS -in | 3 | 3 | 2 199-x -TA -DS -in -RT | 2 | 2 | 1 200in: Fc & (a | b) & GF(a | b) & Gc 201-TGTA | 8 | 34 | XXX 202-TGTA -RT | 8 | 34 | XXX 203-TA | 7 | 21 | 6 204-TA -RT | 7 | 21 | 6 205-TA -lv | 7 | 21 | 3 206-TA -lv -RT | 7 | 21 | 3 207-TA -sp | 7 | 21 | 3 208-TA -sp -RT | 7 | 21 | 3 209-TA -lv -sp | 7 | 21 | 3 210-TA -lv -sp -RT | 7 | 21 | 3 211-TA -DS | 11 | 51 | 10 212-TA -DS -RT | 11 | 51 | 10 213-TA -DS -lv | 11 | 51 | 7 214-TA -DS -lv -RT | 11 | 51 | 7 215-TA -DS -sp | 11 | 51 | 7 216-TA -DS -sp -RT | 11 | 51 | 7 217-TA -DS -lv -sp | 11 | 51 | 7 218-TA -DS -lv -sp -RT | 11 | 51 | 7 219-x -TA -DS -in | 11 | 33 | 5 220-x -TA -DS -in -RT | 11 | 33 | 5 221in: a R (b R c) 222-TGTA | 17 | 124 | XXX 223-TGTA -RT | 6 | 30 | XXX 224-TA | 16 | 95 | 16 225-TA -RT | 6 | 29 | 6 226-TA -lv | 17 | 103 | 14 227-TA -lv -RT | 8 | 42 | 6 228-TA -sp | 16 | 103 | 13 229-TA -sp -RT | 7 | 42 | 5 230-TA -lv -sp | 17 | 103 | 14 231-TA -lv -sp -RT | 8 | 42 | 6 232-TA -DS | 16 | 95 | 16 233-TA -DS -RT | 6 | 29 | 6 234-TA -DS -lv | 16 | 95 | 16 235-TA -DS -lv -RT | 6 | 29 | 6 236-TA -DS -sp | 16 | 95 | 16 237-TA -DS -sp -RT | 6 | 29 | 6 238-TA -DS -lv -sp | 16 | 95 | 16 239-TA -DS -lv -sp -RT | 6 | 29 | 6 240-x -TA -DS -in | 16 | 92 | 16 241-x -TA -DS -in -RT | 6 | 26 | 6 242in: (a U b) U (c U d) 243-TGTA | 77 | 1521 | XXX 244-TGTA -RT | 18 | 409 | XXX 245-TA | 76 | 1210 | 48 246-TA -RT | 29 | 493 | 9 247-TA -lv | 77 | 1418 | 17 248-TA -lv -RT | 31 | 652 | 2 249-TA -sp | 76 | 1418 | 16 250-TA -sp -RT | 30 | 652 | 1 251-TA -lv -sp | 77 | 1418 | 17 252-TA -lv -sp -RT | 31 | 652 | 2 253-TA -DS | 76 | 1210 | 48 254-TA -DS -RT | 30 | 508 | 10 255-TA -DS -lv | 77 | 1418 | 17 256-TA -DS -lv -RT | 31 | 652 | 2 257-TA -DS -sp | 76 | 1418 | 16 258-TA -DS -sp -RT | 30 | 652 | 1 259-TA -DS -lv -sp | 77 | 1418 | 17 260-TA -DS -lv -sp -RT | 31 | 652 | 2 261-x -TA -DS -in | 76 | 1308 | 17 262-x -TA -DS -in -RT | 26 | 500 | 2 263in: ((Gp2)U(F(1)))&(p1 R(p2 R p0)) 264-TGTA | 17 | 124 | XXX 265-TGTA -RT | 6 | 30 | XXX 266-TA | 16 | 95 | 16 267-TA -RT | 6 | 29 | 6 268-TA -lv | 17 | 103 | 14 269-TA -lv -RT | 8 | 42 | 6 270-TA -sp | 16 | 103 | 13 271-TA -sp -RT | 7 | 42 | 5 272-TA -lv -sp | 17 | 103 | 14 273-TA -lv -sp -RT | 8 | 42 | 6 274-TA -DS | 16 | 95 | 16 275-TA -DS -RT | 6 | 29 | 6 276-TA -DS -lv | 16 | 95 | 16 277-TA -DS -lv -RT | 6 | 29 | 6 278-TA -DS -sp | 16 | 95 | 16 279-TA -DS -sp -RT | 6 | 29 | 6 280-TA -DS -lv -sp | 16 | 95 | 16 281-TA -DS -lv -sp -RT | 6 | 29 | 6 282-x -TA -DS -in | 16 | 92 | 16 283-x -TA -DS -in -RT | 6 | 26 | 6 284in: a U (b U c) 285-TGTA | 22 | 196 | XXX 286-TGTA -RT | 6 | 59 | XXX 287-TA | 21 | 144 | 16 288-TA -RT | 9 | 62 | 5 289-TA -lv | 22 | 164 | 9 290-TA -lv -RT | 11 | 85 | 2 291-TA -sp | 21 | 164 | 8 292-TA -sp -RT | 10 | 85 | 1 293-TA -lv -sp | 22 | 164 | 9 294-TA -lv -sp -RT | 11 | 85 | 2 295-TA -DS | 21 | 144 | 16 296-TA -DS -RT | 10 | 69 | 6 297-TA -DS -lv | 22 | 164 | 9 298-TA -DS -lv -RT | 11 | 85 | 2 299-TA -DS -sp | 21 | 164 | 8 300-TA -DS -sp -RT | 10 | 85 | 1 301-TA -DS -lv -sp | 22 | 164 | 9 302-TA -DS -lv -sp -RT | 11 | 85 | 2 303-x -TA -DS -in | 22 | 164 | 9 304-x -TA -DS -in -RT | 11 | 85 | 2 305in: !(Ga U b) 306-TGTA | 11 | 50 | XXX 307-TGTA -RT | 5 | 23 | XXX 308-TA | 10 | 31 | 8 309-TA -RT | 4 | 13 | 3 310-TA -lv | 11 | 37 | 6 311-TA -lv -RT | 6 | 20 | 3 312-TA -sp | 10 | 37 | 5 313-TA -sp -RT | 5 | 20 | 2 314-TA -lv -sp | 11 | 37 | 6 315-TA -lv -sp -RT | 6 | 20 | 3 316-TA -DS | 10 | 31 | 8 317-TA -DS -RT | 5 | 16 | 4 318-TA -DS -lv | 11 | 37 | 7 319-TA -DS -lv -RT | 6 | 20 | 4 320-TA -DS -sp | 10 | 37 | 6 321-TA -DS -sp -RT | 5 | 20 | 3 322-TA -DS -lv -sp | 11 | 37 | 7 323-TA -DS -lv -sp -RT | 6 | 20 | 4 324-x -TA -DS -in | 11 | 37 | 7 325-x -TA -DS -in -RT | 6 | 20 | 4 326in: # Make sure '(G (p -> F q)) && ((X (p) U q) || ! X (p U (p && q)))' 327in: # has 21 states and 96 transitions before minimization, and 328in: # has 20 states and 89 transitions, after minimization. 329in: (G (p -> F q)) && ((X (p) U q) || ! X (p U (p && q))) 330-TGTA | 21 | 127 | XXX 331-TGTA -RT | 17 | 93 | XXX 332-TA | 20 | 92 | 12 333-TA -RT | 15 | 57 | 9 334-TA -lv | 21 | 104 | 6 335-TA -lv -RT | 17 | 75 | 4 336-TA -sp | 20 | 100 | 5 337-TA -sp -RT | 16 | 70 | 3 338-TA -lv -sp | 21 | 104 | 6 339-TA -lv -sp -RT | 17 | 75 | 4 340-TA -DS | 20 | 92 | 13 341-TA -DS -RT | 18 | 81 | 12 342-TA -DS -lv | 21 | 104 | 7 343-TA -DS -lv -RT | 20 | 99 | 7 344-TA -DS -sp | 20 | 100 | 6 345-TA -DS -sp -RT | 19 | 95 | 6 346-TA -DS -lv -sp | 21 | 104 | 7 347-TA -DS -lv -sp -RT | 20 | 99 | 7 348-x -TA -DS -in | 19 | 66 | 5 349-x -TA -DS -in -RT | 15 | 52 | 5 350in: GFa & GFb & GFc & GFd & GFe & GFg 351-TGTA | 65 | 4160 | XXX 352-TGTA -RT | 65 | 4160 | XXX 353-TA | 64 | 4032 | 1 354-TA -RT | 64 | 4032 | 1 355-TA -lv | 64 | 4032 | 1 356-TA -lv -RT | 64 | 4032 | 1 357-TA -sp | 64 | 4032 | 1 358-TA -sp -RT | 64 | 4032 | 1 359-TA -lv -sp | 64 | 4032 | 1 360-TA -lv -sp -RT | 64 | 4032 | 1 361-TA -DS | 448 | 52416 | 70 362-TA -DS -RT | 448 | 52416 | 70 363-TA -DS -lv | 448 | 52416 | 70 364-TA -DS -lv -RT | 448 | 52416 | 70 365-TA -DS -sp | 448 | 52416 | 70 366-TA -DS -sp -RT | 448 | 52416 | 70 367-TA -DS -lv -sp | 448 | 52416 | 70 368-TA -DS -lv -sp -RT | 448 | 52416 | 70 369-x -TA -DS -in | 449 | 28608 | 65 370-x -TA -DS -in -RT | 320 | 20352 | 65 371in: Gq|Gr|(G(q|FGp)&G(r|FG!p)) 372-TGTA | 65 | 842 | XXX 373-TGTA -RT | 21 | 294 | XXX 374-TA | 64 | 740 | 26 375-TA -RT | 22 | 264 | 14 376-TA -lv | 65 | 776 | 15 377-TA -lv -RT | 23 | 288 | 7 378-TA -sp | 64 | 764 | 14 379-TA -sp -RT | 22 | 280 | 6 380-TA -lv -sp | 65 | 776 | 15 381-TA -lv -sp -RT | 23 | 288 | 7 382-TA -DS | 64 | 740 | 34 383-TA -DS -RT | 26 | 366 | 20 384-TA -DS -lv | 65 | 776 | 25 385-TA -DS -lv -RT | 27 | 396 | 13 386-TA -DS -sp | 64 | 764 | 24 387-TA -DS -sp -RT | 26 | 386 | 12 388-TA -DS -lv -sp | 65 | 776 | 25 389-TA -DS -lv -sp -RT | 27 | 396 | 13 390-x -TA -DS -in | 33 | 152 | 19 391-x -TA -DS -in -RT | 21 | 112 | 11 392in: FG((WaitRight4 M (HasRight1 W GWaitLeft0)) M HasLeft4) 393-TGTA | 45 | 730 | XXX 394-TGTA -RT | 35 | 598 | XXX 395-TA | 44 | 602 | 16 396-TA -RT | 33 | 482 | 9 397-TA -lv | 45 | 676 | 9 398-TA -lv -RT | 35 | 566 | 4 399-TA -sp | 44 | 667 | 8 400-TA -sp -RT | 34 | 545 | 3 401-TA -lv -sp | 45 | 676 | 9 402-TA -lv -sp -RT | 35 | 566 | 4 403-TA -DS | 54 | 722 | 26 404-TA -DS -RT | 42 | 608 | 18 405-TA -DS -lv | 55 | 800 | 19 406-TA -DS -lv -RT | 44 | 702 | 13 407-TA -DS -sp | 54 | 789 | 18 408-TA -DS -sp -RT | 43 | 686 | 12 409-TA -DS -lv -sp | 55 | 800 | 19 410-TA -DS -lv -sp -RT | 44 | 702 | 13 411-x -TA -DS -in | 55 | 694 | 11 412-x -TA -DS -in -RT | 41 | 597 | 8 413in: G(F(GWaitLeft7 U Idle4) U (WaitLeft2 M IsEating2)) 414-TGTA | 69 | 1539 | XXX 415-TGTA -RT | 49 | 935 | XXX 416-TA | 68 | 1443 | 16 417-TA -RT | 56 | 1179 | 15 418-TA -lv | 68 | 1443 | 16 419-TA -lv -RT | 56 | 1179 | 15 420-TA -sp | 68 | 1443 | 16 421-TA -sp -RT | 56 | 1179 | 15 422-TA -lv -sp | 68 | 1443 | 16 423-TA -lv -sp -RT | 56 | 1179 | 15 424-TA -DS | 124 | 2964 | 44 425-TA -DS -RT | 96 | 2099 | 42 426-TA -DS -lv | 125 | 3028 | 42 427-TA -DS -lv -RT | 97 | 2149 | 40 428-TA -DS -sp | 124 | 3012 | 41 429-TA -DS -sp -RT | 96 | 2134 | 39 430-TA -DS -lv -sp | 125 | 3028 | 42 431-TA -DS -lv -sp -RT | 97 | 2149 | 40 432-x -TA -DS -in | 125 | 1838 | 25 433-x -TA -DS -in -RT | 87 | 1296 | 25 434EOF 435 436sed -n 's/in: \(.*\)/\1/p' checkta.txt > input.txt 437run 0 ../checkta input.txt | tee output.txt 438diff checkta.txt output.txt 439