import org.jbpt.petri.INetSystem; //导入依赖的package包/类
@Override
@SuppressWarnings("unchecked")
public int storeNetSystem(String pnmlFilePath, String externalID) throws SQLException {
	if (pnmlFilePath==null || externalID==null) return 0;
	
	File pnmlFile = new File(pnmlFilePath);
	
	if (pnmlFile.exists() && pnmlFile.isFile() && pnmlFile.canRead()) {
		try {
			byte[] encoded = Files.readAllBytes(Paths.get(pnmlFilePath));
			String pnmlContent =new String(encoded, StandardCharsets.UTF_8); 
			
			PNMLSerializer PNML = new PNMLSerializer();
			INetSystem<F,N,P,T,M> sys = (INetSystem<F,N,P,T,M>) PNML.parse(pnmlFilePath);
			
			return this.storeNetSystem(pnmlContent, sys, externalID);
		} catch (IOException e) {
			return 0;
		}
	}
	else return 0;
}
 

import org.jbpt.petri.INetSystem; //导入依赖的package包/类
@Override
@SuppressWarnings("unchecked")
public INetSystem<F,N,P,T,M> restoreNetSystem(int internalID) throws SQLException {
	String pnmlContent = this.restorePNMLContent(internalID);
	
	if (pnmlContent == null) return null;
	
	PNMLSerializer PNML = new PNMLSerializer();
	INetSystem<F,N,P,T,M> result = (INetSystem<F,N,P,T,M>)PNML.parse(pnmlContent.getBytes());
	
	// set proper names
	int pi,ti;
	pi = ti = 1;
	
	for (P p : result.getPlaces()) {
		p.setName("p"+pi++);
	}
	
	for (T t : result.getTransitions()) {
		t.setName("t"+ti++);
	}
	
	return result;
}
 

import org.jbpt.petri.INetSystem; //导入依赖的package包/类
public int getNumberOfPlaces(String externalID)
{
	int result = 0;
	int internalID = 0;
	INetSystem<F,N,P,T,M> sys = null;
	
	try {
	
		internalID = this.getInternalID(externalID);
		sys = this.restoreNetSystem(internalID);
	
		} catch (SQLException e) {e.printStackTrace();}
	
	result =  sys.getPlaces().size();
	
	return result;
}
 

import org.jbpt.petri.INetSystem; //导入依赖的package包/类
@Override
public boolean isReachable(INetSystem<F,N,P,T,M> sys, Collection<P> marking) {
	if (sys==null) return false;
	for (P p : marking)
		if (!sys.getPlaces().contains(p)) return false;
	
	String pred = "";			
	Iterator<P> i = sys.getPlaces().iterator();
	P place = i.next();
	pred += place.getName() + " = " + Collections.frequency(marking,place);
	while (i.hasNext()) {
		pred += " AND ";
		place = i.next();
		pred += place.getName() + " = " + Collections.frequency(marking,place);
	}
	
	return this.isReachable(sys, pred);
}
 

import org.jbpt.petri.INetSystem; //导入依赖的package包/类
@SuppressWarnings("unchecked")
private Set<P> getMarking(PQLAlignment alignment, int j, INetSystem<F,N,P,T,M> system)
	{
		system.loadNaturalMarking();
		Set<P> marking = null;
			
		for(int i=0; i<=j; i++)
		{
			PQLMove move = alignment.getAlignment().get(i);
			T t = null;
			
			if(!move.getMoM().equals("SKIP_STEP"))
			t = (T) move.getT();
			
			if(t != null)
			{
			system.fire(t);
			}
		}
			
		marking = system.getMarkedPlaces();
	
		return marking;

	}
 

import org.jbpt.petri.INetSystem; //导入依赖的package包/类
@Override
public void configure(Object obj) throws PQLException {
	if (obj == null) throw new PQLException("Configuration object is NULL.");
	
	if (!(obj instanceof INetSystem)) throw new PQLException("Configuration object is not an INetSystem.");
	
	INetSystem<F,N,P,T,M> originalNetSystem = (INetSystem<F,N,P,T,M>) obj;
	
	PetriNetStructuralChecks<F,N,P,T> check = new PetriNetStructuralChecks<F,N,P,T>();
	boolean wf = check.isWorkflowNet(originalNetSystem);
	if (!wf) throw new PQLException("Configuration object is not a workflow net.");
	
	this.n2n.clear();
	this.clonedNetSystem = originalNetSystem.clone(this.n2n);
	this.sinkPlace = this.clonedNetSystem.getSinkPlaces().iterator().next();
	this.TM = new AbstractNetSystemTransformationManager<F,N,P,T,M>(this.clonedNetSystem);
}
 

import org.jbpt.petri.INetSystem; //导入依赖的package包/类
@Override
protected void constructRuns(INetSystem<F,N,P,T,M> system) {
	switch (this.setup.SIGNIFICANCE_CHECK) {
		case EXHAUSTIVE:
			this.constructRunsExhaustive(system);
			break;
		case HASHMAP_BASED:
			this.constructRunsHashmapBased(system);
			break;
		case TREE_OF_RUNS:
			this.constructRunsTreeOfRuns(system);
			break;
		default:
			this.constructRunsExhaustive(system);
	}
}
 

import org.jbpt.petri.INetSystem; //导入依赖的package包/类
@Override
protected void constructRuns(INetSystem<F,N,P,T,M> system) {
	map2 = new HashMap<N, N>();
	this.reducedSys = system.clone(map2);
	
	map = new HashMap<N, N>();
	for (Map.Entry<N,N> entry : map2.entrySet())
		map.put(entry.getValue(), entry.getKey());
	
	try {		
		abs = this.reduce(this.reducedSys);
	}
	catch(Exception e) {
		System.err.println(e.getMessage());
	}
	
	super.constructRuns(this.reducedSys);
}
 

import org.jbpt.petri.INetSystem; //导入依赖的package包/类
/**
 * Constructor of a representative untangling.
 * 
 * @param sys Net system to untangle.
 */
public AbstractRepresentativeUntangling(INetSystem<F,N,P,T,M> sys, UntanglingSetup setup) {
	if (sys==null) return;
	
	this.setup = setup;
	
	this.sys = sys;
	this.runs = new HashSet<IRun<F, N, P, T, M>>();
	
	long start = System.nanoTime();
	this.constructRuns(this.sys);
	long stop = System.nanoTime();
	this.time = stop - start;
	
	if (this.setup.SIGNIFICANCE_CHECK == SignificanceCheckType.TREE_OF_RUNS) {
		for (TreeStep<F,N,P,T,M> step : this.torLeaves) {
			IRun<F,N,P,T,M> run = this.constructRun(step);
			this.runs.add(run);
		}
	}
	
	this.constructProcesses();
}
 

import org.jbpt.petri.INetSystem; //导入依赖的package包/类
private IRun<F,N,P,T,M> constructRun(TreeStep<F,N,P,T,M> step) {
	List<TreeStep<F,N,P,T,M>> list = new ArrayList<TreeStep<F, N, P, T, M>>();
	TreeStep<F,N,P,T,M> s = step;
	list.add(s);
	while (s.getParent()!=null) {
		s = s.getParent();
		list.add(0,s);
	}
	
	INetSystem<F,N,P,T,M> netSystem = (this.reducedSys==null) ? this.sys : this.reducedSys;
	IRun<F,N,P,T,M> run = this.createRun(netSystem);
	for (TreeStep<F,N,P,T,M> ss : list) {
		if (ss.getTransition()!=null)
			run.append(ss.getTransition());
	}
	
	return run;
}
 

import org.jbpt.petri.INetSystem; //导入依赖的package包/类
@Override
public boolean isSoundWorkflowNet(INetSystem<F,N,P,T,M> sys) {
	if (sys==null) return false;
	
	PetriNetStructuralChecks<F,N,P,T> check = new PetriNetStructuralChecks<F,N,P,T>();
	boolean wf = check.isWorkflowNet(sys);
	
	if (!wf) return false;
	
	P i = sys.getSourcePlaces().iterator().next();
	P o = sys.getSinkPlaces().iterator().next();
	
	for (P p : sys.getPlaces()) {
		if (p.equals(i)) {
			if (sys.getMarking().get(p)!=1) return false;
		} else {
			if (sys.getMarking().get(p)!=0) return false;
		}
	}
	
	T t = sys.createTransition();
	t.setName("TEMP");
	
	sys.addTransition(t);
	sys.addFlow(o,t);
	sys.addFlow(t,i);
		
	boolean result = true;
	
	if (!this.isBounded(sys)) result = false;
	
	if (result)
		if (!this.isLive(sys)) result = false;
	
	sys.removeTransition(t);
	
	return result;
}
 

import org.jbpt.petri.INetSystem; //导入依赖的package包/类
public boolean isLive(INetSystem<F,N,P,T,M> sys, Set<Process> p) {
	if (sys==null) return false;
	
	for (T t : sys.getTransitions()) {
		if (!this.isLive(sys, t, p))
			return false;
	}
	
	return true;
}
 

import org.jbpt.petri.INetSystem; //导入依赖的package包/类
@Override
public boolean isBounded(INetSystem<F,N,P,T,M> sys) {
	if (sys==null) return false;
	
	for (P p : sys.getPlaces()) {
		if (!this.isBounded(sys,p))
			return false;
	}
	
	return true;
}
 

import org.jbpt.petri.INetSystem; //导入依赖的package包/类
@Override
public boolean check(INetSystem<F,N,P,T,M> sys, String property) {
	if (sys==null) return false;
	
	boolean result = false;
	
	try 
    {
		String[] cmds = {this.lolaPath, "--formula="+property, "--quiet", "--json"};
		Process p = Runtime.getRuntime().exec(cmds);
		
		BufferedReader input	= new BufferedReader(new InputStreamReader(p.getInputStream()));
		BufferedWriter output	= new BufferedWriter(new OutputStreamWriter(p.getOutputStream()));			
		
		String net = this.sys2lola(sys);
		// System.out.println(net); // debug
		output.write(net);
		output.close();
		
		String jsonString = "";
		String line;
		while ((line = input.readLine()) != null) {
			jsonString += line;
		}
		input.close();
		
		JSONObject json = new JSONObject(jsonString);
		
		//System.out.println(jsonString); // debug
		if (json.getJSONObject("analysis").get("result").toString().equals("true"))
			result = true;
    } 
    catch(Exception e) {}
		
	return result;
}
 

import org.jbpt.petri.INetSystem; //导入依赖的package包/类
public SimpleStateSpace(INetSystem<F, N, P, T, M> netSystem) {
	super();
	this.netSystem = netSystem;
	this.enabled = new HashMap<M, Set<T>>();
	this.toVisit = new HashMap<M, Set<T>>();
	this.stateTransitions = new HashMap<M, Map<T, M>>();
}
 

import org.jbpt.petri.INetSystem; //导入依赖的package包/类
public AbstractUntanglingBasedBehavioralQuerying(INetSystem<F,N,P,T,M> sys) {
	super(sys);
	
	UntanglingSetup setup = new UntanglingSetup();
	setup.REDUCE = false;
	setup.ISOMORPHISM_REDUCTION = false;
	setup.SIGNIFICANCE_CHECK = SignificanceCheckType.TREE_OF_RUNS;
	
	this.repUnt = new AbstractReductionBasedRepresentativeUntangling<BPN, C, E, F, N, P, T, M>(this.sys,setup);
	this.untangling = repUnt.getProcesses();
	
}
 

import org.jbpt.petri.INetSystem; //导入依赖的package包/类
public TreeStep(INetSystem<F,N,P,T,M> system, TreeStep<F,N,P,T,M> parent, M inputMarking, T transition, M outputMarking, int position) {
	this.system = system;
	
	this.parent = parent;
	this.inputMarking = inputMarking;
	this.transition = transition;
	this.outputMarking = outputMarking;
	
	this.position = position;
}
 

import org.jbpt.petri.INetSystem; //导入依赖的package包/类
public ProjectedStateSpace(INetSystem<F, N, P, T, M> netSystem, Set<T> projectionSet) {
	super();
	this.netSystem = netSystem;
	this.enabled = new HashMap<M, Set<T>>();
	this.txM = new HashMap<T, Set<M>>();
	this.vTxM = new HashMap<T, Set<M>>();
	this.stateTransitions = new HashMap<M, Map<T, M>>();

	this.projectionSetForStepMatrix = new HashMap<T, Integer>();
	
	/*
	 * All transitions in the projection set get an id
	 * for the step matrix
	 */
	List<T> tmpList = new ArrayList<T>(projectionSet);
	for (int i = 0; i < tmpList.size(); i++) 
		this.projectionSetForStepMatrix.put(tmpList.get(i), i); 

	/*
	 * Init the step matrix
	 */
	this.stepMatrix = new boolean[projectionSetForStepMatrix.keySet().size()][projectionSetForStepMatrix.keySet().size()];
	for (int i = 0; i < projectionSetForStepMatrix.keySet().size(); i++) {
		this.stepMatrix[i][i] = false;
		for (int j = i + 1; j < projectionSetForStepMatrix.keySet().size(); j++) {
			this.stepMatrix[i][j] = false;
			this.stepMatrix[j][i] = false;
		}
	}
}
 

import org.jbpt.petri.INetSystem; //导入依赖的package包/类
public int getNumberOfTransitions(String externalID)
{
	int result = 0;
	
	int internalID = 0;
	INetSystem<F,N,P,T,M> sys = null;
	
	try {
	
		internalID = this.getInternalID(externalID);
		sys = this.restoreNetSystem(internalID);
	
		} catch (SQLException e) {e.printStackTrace();}
	
	result =  sys.getTransitions().size();
	
	return result;
}
 

import org.jbpt.petri.INetSystem; //导入依赖的package包/类
public int getNumberOfFlowArcs(String externalID)
{
	int result = 0;
	
	int internalID = 0;
	INetSystem<F,N,P,T,M> sys = null;
	
	try {
	
		internalID = this.getInternalID(externalID);
		sys = this.restoreNetSystem(internalID);
	
		} catch (SQLException e) {e.printStackTrace();}
	
	result =  sys.getFlow().size();
	
	return result;
}