001/* Compute the alternating simulation of two interface automata.
002
003 Copyright (c) 1999-2016 The Regents of the University of California.
004 All rights reserved.
005 Permission is hereby granted, without written agreement and without
006 license or royalty fees, to use, copy, modify, and distribute this
007 software and its documentation for any purpose, provided that the above
008 copyright notice and the following two paragraphs appear in all copies
009 of this software.
010
011 IN NO EVENT SHALL THE UNIVERSITY OF CALIFORNIA BE LIABLE TO ANY PARTY
012 FOR DIRECT, INDIRECT, SPECIAL, INCIDENTAL, OR CONSEQUENTIAL DAMAGES
013 ARISING OUT OF THE USE OF THIS SOFTWARE AND ITS DOCUMENTATION, EVEN IF
014 THE UNIVERSITY OF CALIFORNIA HAS BEEN ADVISED OF THE POSSIBILITY OF
015 SUCH DAMAGE.
016
017 THE UNIVERSITY OF CALIFORNIA SPECIFICALLY DISCLAIMS ANY WARRANTIES,
018 INCLUDING, BUT NOT LIMITED TO, THE IMPLIED WARRANTIES OF
019 MERCHANTABILITY AND FITNESS FOR A PARTICULAR PURPOSE. THE SOFTWARE
020 PROVIDED HEREUNDER IS ON AN "AS IS" BASIS, AND THE UNIVERSITY OF
021 CALIFORNIA HAS NO OBLIGATION TO PROVIDE MAINTENANCE, SUPPORT, UPDATES,
022 ENHANCEMENTS, OR MODIFICATIONS.
023
024 PT_COPYRIGHT_VERSION_2
025 COPYRIGHTENDKEY
026 */
027package ptolemy.domains.modal.kernel.test;
028
029import java.net.URL;
030import java.util.Iterator;
031import java.util.Set;
032
033import ptolemy.actor.gui.ConfigurationApplication;
034import ptolemy.domains.modal.kernel.ia.InterfaceAutomaton;
035import ptolemy.domains.modal.kernel.ia.StatePair;
036import ptolemy.moml.MoMLParser;
037import ptolemy.util.StringUtilities;
038
039///////////////////////////////////////////////////////////////////
040//// AlternatingSimulation
041
042/**
043 Compute the alternating simulation of two interface automata.
044 This class reads the MoML description of a super automaton and a sub automaton,
045 computes the unique maximal alternating simulation relation from the
046 sub automaton to the super one, then lists all the state pairs in the relation
047 to stdout. The usage is:
048 <pre>
049 java ptolemy.domains.modal.kernel.test.AlternatingSimulation [-reacheable] <i>super_automaton.xml</i> <i>sub_automaton.xml</i>
050 </pre>
051 -reacheable indicates to only list the reacheable alternating simulation state
052 pairs. This flag is optional.
053
054 @author Yuhong Xiong
055 @version $Id$
056 @since Ptolemy II 8.0
057 @Pt.ProposedRating Red (yuhong)
058 @Pt.AcceptedRating Red (reviewmoderator)
059 */
060public class AlternatingSimulation {
061    /** Compute the alternating simulation from the sub automaton to the
062     *  super one and list the result to stdout.
063     *  @param superMoML The MoML file name for the super interface automaton.
064     *  @param subMoML The MoML file name for the sub interface automaton.
065     *  @param onlyReacheable True to indicate only print the reacheable
066     *   state pairs.
067     *  @exception Exception If the specified automata cannot be constructed.
068     */
069    public AlternatingSimulation(String superMoML, String subMoML,
070            boolean onlyReacheable) throws Exception {
071        // Construct the super automaton
072        URL url = ConfigurationApplication.specToURL(superMoML);
073
074        // following the comments in MoMLApplication, use the same URL for
075        // the two arguments (base and URL) to parse().
076        MoMLParser parser = new MoMLParser();
077        InterfaceAutomaton superAutomaton = (InterfaceAutomaton) parser
078                .parse(url, url);
079        superAutomaton.addPorts();
080
081        // Construct the sub automaton
082        url = ConfigurationApplication.specToURL(subMoML);
083
084        // following the comments in MoMLApplication, use the same URL for
085        // the two arguments (base and URL) to parse().  Also, a new instance
086        // of MoMLParser must be used to parse each file, otherwise
087        // the same automaton will be returned the second time parse() is
088        // called.
089        parser = new MoMLParser();
090
091        InterfaceAutomaton subAutomaton = (InterfaceAutomaton) parser.parse(url,
092                url);
093        subAutomaton.addPorts();
094
095        // Compute alternating simulation
096        Set alternatingSimulation = superAutomaton
097                .computeAlternatingSimulation(subAutomaton);
098
099        if (onlyReacheable) {
100            alternatingSimulation = InterfaceAutomaton
101                    .reacheableAlternatingSimulation(alternatingSimulation,
102                            superAutomaton, subAutomaton);
103        }
104
105        // Display result
106        if (alternatingSimulation.isEmpty()) {
107            System.out.println("No alternating simulation between the "
108                    + "specified automata.");
109        } else {
110            System.out.println("Alternating simulation (state_in_"
111                    + superAutomaton.getName() + " - state_in_"
112                    + subAutomaton.getName() + "):");
113
114            Iterator pairs = alternatingSimulation.iterator();
115
116            while (pairs.hasNext()) {
117                StatePair pair = (StatePair) pairs.next();
118                System.out.println(pair.toString());
119            }
120        }
121    }
122
123    ///////////////////////////////////////////////////////////////////
124    ////                         public methods                    ////
125
126    /** Pass the command line arguments to the constructor. The command line
127     *  arguments are an optional flag and two MoML files for
128     *  interface automaton.
129     *  @param args The command line arguments.
130     */
131    public static void main(String[] args) {
132        boolean onlyReacheable = false;
133        String superMoML = null;
134        String subMoML = null;
135
136        if (args.length == 2) {
137            superMoML = args[0];
138            subMoML = args[1];
139        } else if (args.length == 3) {
140            if (args[0].equals("-reacheable")) {
141                onlyReacheable = true;
142                superMoML = args[1];
143                subMoML = args[2];
144            }
145        } else {
146            _printUsageAndExit();
147        }
148
149        try {
150            new AlternatingSimulation(superMoML, subMoML, onlyReacheable);
151        } catch (Exception exception) {
152            System.out.println(exception.getClass().getName() + ": "
153                    + exception.getMessage());
154            exception.printStackTrace();
155        }
156    }
157
158    ///////////////////////////////////////////////////////////////////
159    ////                         private methods                   ////
160    private static void _printUsageAndExit() {
161        System.out.println("Usage: java ptolemy.domains.modal.kernel."
162                + "test.AlternatingSimulation <-reacheable> "
163                + "<super_automaton.xml> <sub_automaton.xml>");
164        System.out.println("-reacheable indicates to only print out "
165                + "the reacheable alternating simulation state pairs. "
166                + "This is optional.");
167        System.out.println("super_automaton.xml and sub_automaton.xml "
168                + "are the MoML files for the super and sub automata. "
169                + "They must be present.");
170        StringUtilities.exit(1);
171    }
172}