package de.uni.freiburg.iig.telematik.swat.lukas.modelchecker.adapter.prism.modelconvertor;

import java.util.HashSet;
import java.util.LinkedList;
import java.util.Set;

import de.invation.code.toval.types.Multiset;
import de.uni.freiburg.iig.telematik.sepia.mg.ifnet.IFNetMarkingGraphRelation;
import de.uni.freiburg.iig.telematik.sepia.mg.ifnet.IFNetMarkingGraphState;
import de.uni.freiburg.iig.telematik.sepia.petrinet.AbstractPetriNet;
import de.uni.freiburg.iig.telematik.sepia.petrinet.ifnet.IFNet;
import de.uni.freiburg.iig.telematik.sepia.petrinet.ifnet.IFNetFlowRelation;
import de.uni.freiburg.iig.telematik.sepia.petrinet.ifnet.IFNetMarking;
import de.uni.freiburg.iig.telematik.sepia.petrinet.ifnet.IFNetPlace;
import de.uni.freiburg.iig.telematik.sepia.petrinet.ifnet.abstr.AbstractIFNet;
import de.uni.freiburg.iig.telematik.sepia.petrinet.ifnet.abstr.AbstractIFNetFlowRelation;
import de.uni.freiburg.iig.telematik.sepia.petrinet.ifnet.abstr.AbstractIFNetPlace;
import de.uni.freiburg.iig.telematik.sepia.petrinet.ifnet.abstr.AbstractIFNetTransition;


public class IFNetConverter extends CPNConverter {

	private AbstractIFNet<?,?,?,?,?,?,?,?> mNet;

	public IFNetConverter(IFNet net) {
		super(net);
	}
	
	@SuppressWarnings("static-access")
	@Override
	protected StringBuilder createPlaceVars() {
		
		StringBuilder allPlacesBuilder = new StringBuilder();
		
		for (AbstractIFNetPlace<?> p : mNet.getPlaces()) {
			
			StringBuilder placeBuilder = new StringBuilder();

			placeBuilder.append("//PlaceName: " + p.getName() +" (PlaceLabel: " + p.getLabel() +")" + "\n");
			
			if (!mNet.getSourcePlaces().contains(p)) {
			
				if (mNet.getDrainPlaces().contains(p)) {
					placeBuilder.append("//drainPlace" + "\n");
				}
				
				LinkedList<AbstractIFNetFlowRelation<?,?>> inRelations = 
						new LinkedList<AbstractIFNetFlowRelation<?,?>>(p.getIncomingRelations());
				Set<String> possibleColors = new HashSet<String>();
				
				if(mNet.getInitialMarking().get(p.getName()) != null) {
					possibleColors.addAll(mNet.getInitialMarking().get(p.getName()).support());
                }
				
				for (AbstractIFNetFlowRelation<?,?> inRel : inRelations) {
					possibleColors.addAll(inRel.getConstraint().support());
				}
				
				for(String color : possibleColors){
					placeBuilder.append(p.getName() +"_" + color + " : ");
					if (p.getColorCapacity(color) != -1) {
						placeBuilder.append("[0.." + p.getColorCapacity(color) + "] ");
					} else {
						System.out.println("Not a valid CWN! Place " + p.getName() + "is not bounded.");
					}
					
					if (mNet.getInitialMarking().get(p.getName()) != null) {
						placeBuilder.append("init " + mNet.getInitialMarking().get(
								p.getName()).multiplicity(color) + ";" + "\n");
					} else {
						placeBuilder.append("init 0;" + "\n");
					}
				}
				} else {
					
				placeBuilder.append("//SourcePlace" + "\n");
				Set<String> possibleColors = new HashSet<String>();
				Multiset<String> possibleColorMultiSet = mNet.getInitialMarking().get(p.getName()); 
				possibleColors.addAll(possibleColorMultiSet.support());
							
				for (String color : possibleColors) {
					placeBuilder.append(p.getName() + "_" + color + 
							" : [0.." + p.getColorCapacity(color) + "] init " + 
							possibleColorMultiSet.multiplicity(color) + ";" + "\n");
				}
			}
			
			allPlacesBuilder.append(placeBuilder.append("\n"));
			
		}
				
		return allPlacesBuilder;
	}

}

@@ -257,472 +257,28 @@
 pia.
-mg.ifnet.IFNetMarkingGraphRelation;%0Aimport de.uni.freiburg.iig.telematik.sepia.mg.ifnet.IFNetMarkingGraphState;%0Aimport de.uni.freiburg.iig.telematik.sepia.petrinet.AbstractPetriNet;%0Aimport de.uni.freiburg.iig.telematik.sepia.petrinet.ifnet.IFNet;%0Aimport de.uni.freiburg.iig.telematik.sepia.petrinet.ifnet.IFNetFlowRelation;%0Aimport de.uni.freiburg.iig.telematik.sepia.petrinet.ifnet.IFNetMarking;%0Aimport de.uni.freiburg.iig.telematik.sepia.petrinet.ifnet.IFNetPlace
+petrinet.ifnet.IFNet
 ;%0Aim
@@ -533,97 +533,8 @@
 ce;%0A
-import de.uni.freiburg.iig.telematik.sepia.petrinet.ifnet.abstr.AbstractIFNetTransition;%0A
 %0A%0Apu
@@ -666,16 +666,16 @@
  net) %7B%0A
-
 %09%09super(
@@ -680,16 +680,30 @@
 r(net);%0A
+%09%09mNet = net;%0A
 %09%7D%0A%09%0A%09@S

fix for IFNetConverter. Private field was never set