1#!/bin/sh 2# -*- coding: utf-8 -*- 3# Copyright (C) 2008, 2009, 2013, 2014, 2016 Laboratoire de Recherche et 4# Développement de l'Epita (LRDE). 5# Copyright (C) 2003, 2004, 2005 Laboratoire d'Informatique de 6# Paris 6 (LIP6), département Systèmes Répartis Coopératifs (SRC), 7# Université Pierre et Marie Curie. 8# 9# This file is part of Spot, a model checking library. 10# 11# Spot is free software; you can redistribute it and/or modify it 12# under the terms of the GNU General Public License as published by 13# the Free Software Foundation; either version 3 of the License, or 14# (at your option) any later version. 15# 16# Spot is distributed in the hope that it will be useful, but WITHOUT 17# ANY WARRANTY; without even the implied warranty of MERCHANTABILITY 18# or FITNESS FOR A PARTICULAR PURPOSE. See the GNU General Public 19# License for more details. 20# 21# You should have received a copy of the GNU General Public License 22# along with this program. If not, see <http://www.gnu.org/licenses/>. 23 24 25. ./defs 26 27set -e 28 29cat >input1 <<EOF 30HOA: v1 31States: 3 32Start: 0 33AP: 3 "a" "b" "c" 34acc-name: Buchi 35Acceptance: 1 Inf(0) 36properties: trans-labels explicit-labels state-acc 37--BODY-- 38State: 0 {0} 39[0] 1 40[1] 2 41State: 1 42State: 2 {0} 43[!0] 0 44[2] 1 45--END-- 46EOF 47 48cat >input2 <<EOF 49HOA: v1 50States: 2 51Start: 0 52AP: 2 "b" "a" 53acc-name: generalized-Buchi 2 54Acceptance: 2 Inf(0)&Inf(1) 55properties: trans-labels explicit-labels state-acc deterministic 56--BODY-- 57State: 0 {0} 58[0] 1 59State: 1 {1} 60[1] 0 61--END-- 62EOF 63 64cat >expected <<EOF 65HOA: v1 66States: 4 67Start: 0 68AP: 3 "b" "a" "c" 69acc-name: generalized-Buchi 3 70Acceptance: 3 Inf(0)&Inf(1)&Inf(2) 71properties: trans-labels explicit-labels state-acc 72--BODY-- 73State: 0 {0 1} 74[0&1] 1 75[0] 2 76State: 1 77State: 2 {0 2} 78[1&2] 3 79State: 3 80--END-- 81EOF 82 83run 0 autfilt input1 --product input2 --hoa | tee stdout 84diff stdout expected 85 86cat >expected <<EOF 87HOA: v1 88States: 1 89Start: 0 90AP: 0 91acc-name: all 92Acceptance: 0 t 93properties: trans-labels explicit-labels state-acc deterministic 94--BODY-- 95State: 0 96--END-- 97EOF 98 99run 0 autfilt input1 --product input2 --hoa --small | tee stdout 100run 0 autfilt -F stdout --isomorph expected 101 102# Reading two automata from stdin 103ltl2tgba '!a' 'a U b' | autfilt --product=- - > aut1 104ltl2tgba '!a&b' | autfilt -q --equivalent-to=aut1 105