uppaal-4.1.19.zip

内容包含Uppaal工具，及简单教程，注意必须提前安装好Java1.8及以上环境，运行uppaal.jar，即可运行Uppaal。时间自动机是一套对实时系统进行建模和验证的理论。这一理论是Alur和Dill的杰出工作成果。很多验证工具（例如Uppaal）就是基于时间自动机理论制作的。

/**
 * A sample Java code demonstrating the use of lib/model.jar in Uppaal-4.1.19 distribution.
 * Use the following commands to compile and run:
 *
 *     javac -cp lib/model.jar ModelDemo.java
 *     java -cp uppaal.jar:lib/model.jar:. ModelDemo hardcoded
 *
 * ModelDemo will produce result.xml and generate a symbolic trace.
 * ModelDemo can also read an external model file （use Control+C to stop）:
 *
 *     java -cp uppaal.jar:lib/model.jar:. ModelDemo demo/train-gate.xml
 *
 * @author Marius Mikucionis marius@cs.aau.dk
 */

import com.uppaal.engine.CannotEvaluateException;
import com.uppaal.engine.Engine;
import com.uppaal.engine.EngineException;
import com.uppaal.engine.Problem;
import com.uppaal.model.core2.Document;
import com.uppaal.model.core2.Edge;
import com.uppaal.model.core2.Location;
import com.uppaal.model.core2.Property;
import com.uppaal.model.core2.PrototypeDocument;
import com.uppaal.model.core2.Template;
import com.uppaal.model.system.SystemEdge;
import com.uppaal.model.system.SystemLocation;
import com.uppaal.model.system.SystemState;
import com.uppaal.model.system.concrete.ConcreteState;
import com.uppaal.model.system.concrete.ConcreteVariable;
import com.uppaal.model.system.symbolic.SymbolicState;
import com.uppaal.model.system.symbolic.SymbolicTransition;
import com.uppaal.model.system.UppaalSystem;
import java.math.BigDecimal;
import java.io.IOException;
import java.io.File;
import java.net.MalformedURLException;
import java.net.URL;
import java.util.ArrayList;
import java.util.List;

public class ModelDemo
{
    /**
     * Valid kinds of labels on locations.
     */
    public enum LKind {
        name init urgent committed invariant exponentialrate comments
    };
    /**
     * Valid kinds of labels on edges.
     */
    public enum EKind {
        select guard synchronisation assignment comments
    };
    /**
     * Sets a label on a location.
     * @param l the location on which the label is going to be attached
     * @param kind a kind of the label
     * @param value the label value （either boolean or String）
     * @param x the x coordinate of the label
     * @param y the y coordinate of the label
     */
    public static void setLabel（Location l LKind kind object value int x int y） {
        l.setProperty（kind.name（） value）;
        Property p = l.getProperty（kind.name（））;
        p.setProperty（“x“ x）;
        p.setProperty（“y“ y）;        
    }
    /**
     * Adds a location to a template.
     * @param t the template
     * @param name a name for the new location
     * @param x the x coordinate of the location
     * @param y the y coordinate of the location
     * @return the new location instance
     */
    public static Location addLocation（Template t String name int x int y） {
        Location l = t.createLocation（）;
        t.insert（l null）;
        l.setProperty（“x“ x）;
        l.setProperty（“y“ y）;        
        setLabel（l LKind.name name x y-28）;
        return l;
   

 属性            大小     日期    时间   名称
----------- ---------  ---------- -----  ----
     目录           0  2019-11-13 15:05  uppaal-4.1.19\
     文件        4222  2019-11-12 10:40  uppaal-4.1.19\Addlinks.sh
     文件        7322  2019-11-12 10:40  uppaal-4.1.19\Addlinks.vbs
     目录           0  2019-11-12 10:41  uppaal-4.1.19\bin-Linux\
     文件     6024220  2019-11-12 10:41  uppaal-4.1.19\bin-Linux\server
     文件      628112  2019-11-12 10:40  uppaal-4.1.19\bin-Linux\socketserver
     文件     6134908  2019-11-12 10:41  uppaal-4.1.19\bin-Linux\verifyta
     目录           0  2019-11-12 10:41  uppaal-4.1.19\bin-Win32\
     文件     4368384  2019-11-12 10:41  uppaal-4.1.19\bin-Win32\server.exe
     文件     4471296  2019-11-12 10:41  uppaal-4.1.19\bin-Win32\verifyta.exe
     目录           0  2019-11-12 10:41  uppaal-4.1.19\demo\
     文件        5520  2019-11-12 10:41  uppaal-4.1.19\demo\2doors.xml
     文件       11705  2019-11-12 10:41  uppaal-4.1.19\demo\ModelDemo.java
     文件       12777  2019-11-12 10:41  uppaal-4.1.19\demo\Schedulingframework.xml
     文件        4558  2019-11-12 10:41  uppaal-4.1.19\demo\bridge.xml
     文件        2482  2019-11-12 10:41  uppaal-4.1.19\demo\fischer.xml
     文件        2298  2019-11-12 10:41  uppaal-4.1.19\demo\fischer_symmetry.xml
     文件        4420  2019-11-12 10:41  uppaal-4.1.19\demo\interrupt.xml
     文件        5065  2019-11-12 10:41  uppaal-4.1.19\demo\lsc_example.xml
     文件        8299  2019-11-12 10:41  uppaal-4.1.19\demo\lsc_train-gate_parameters.xml
     文件        6228  2019-11-12 10:41  uppaal-4.1.19\demo\scheduling3.xml
     文件       10385  2019-11-12 10:41  uppaal-4.1.19\demo\scheduling4.xml
     目录           0  2019-11-12 10:41  uppaal-4.1.19\demo\smc\
     文件        6070  2019-11-12 10:41  uppaal-4.1.19\demo\smc\ClientServer.xml
     文件        7050  2019-11-12 10:41  uppaal-4.1.19\demo\smc\ball.xml
     文件       19753  2019-11-12 10:41  uppaal-4.1.19\demo\smc\bluetooth.cav.xml
     文件       13661  2019-11-12 10:41  uppaal-4.1.19\demo\smc\csma-ca.xml
     文件       13823  2019-11-12 10:41  uppaal-4.1.19\demo\smc\dice.xml
     文件        3817  2019-11-12 10:41  uppaal-4.1.19\demo\smc\ex-proba1.xml
     文件        4051  2019-11-12 10:41  uppaal-4.1.19\demo\smc\ex-proba2.xml
     文件       23552  2019-11-12 10:41  uppaal-4.1.19\demo\smc\firewire.cav.xml
............此处省略125个文件信息