/**
?*?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個文件信息