plugins/sba/org.polarsys.chess.statebased/ATL/IDM2PNML.atl

-----------------------------------------------------------------------
-- Copyright (C) 2015-2016                                           --
-- University of Firenze, Italy                                      --
--                                                                   --
-- All rights reserved. This program and the accompanying materials  --
-- are made available under the terms of the Eclipse Public License  --
-- v1.0 which accompanies this distribution, and is available at     --
-- http://www.eclipse.org/legal/epl-v10.html                         --
--                                                                   --
-- Contributors:                                                     --
-- Leonardo Montecchi 	lmontecchi@unifi.it                          --
-----------------------------------------------------------------------

-- @atlcompiler atl2010

-- @path IDM=/org.polarsys.chess.statebased/metamodels/IM2.ecore
-- @path PNML=/org.polarsys.chess.statebased/metamodels/placeTransition.ecore

module IDM2PNML;
create OUT : PNML from IN : IDM;

helper def: trCount : Integer = 1;
helper def: placeCount : Integer = 1;
helper def: arcCount : Integer = 1;
helper def: otherCount : Integer = 1;
helper def: timePoints : OrderedSet(Real) = OrderedSet{};

helper def: priTransientDuration : Integer = 4;
helper def: priPropagation : Integer = 5;
helper def: priPropagationChoice : Integer = 7;
helper def: priReset : Integer = 6;
helper def: priActivity : Integer = 2;
helper def: priActivitySchedule : Integer = 1;
helper def: priActivityOutcome : Integer = 3;
helper def: priReliability : Integer = 8;

helper def: getPage : PNML!Page = IDM!Sistema.allInstances()->first();

helper def: tmpLogicExp : PNML!LogicalExpression = OclUndefined;

helper context IDM!NamedElement def: toString() : String = self.Name;
helper context IDM!Error def: toString() : String = self.Name;
helper context IDM!FailureMode def: toString() : String = self.Name;

helper context IDM!Component def: getResetTransition() : PNML!GSPNTransition =
	thisModule.resolveTemp(self, 'reset');
helper context IDM!Threat def: getResetTransition() : PNML!GSPNTransition =
	self.refImmediateComposite().getResetTransition();

helper context PNML!Place def: toString() : String = self.id;
helper context PNML!Transition def: toString() : String = self.id;

helper context PNML!GSPNArc def: defaultID() : String =
	if self.type = #inhibitor then
		self.source.id + '_inhibit_' + self.target.id
	else
		self.source.id + '_to_' + self.target.id
	endif;

rule Sistema {
	from
		s : IDM!Sistema
	to
		pp: PNML!Page (
			id <- s.Name + '_page',
			objects <- Sequence{}
		),
		net: PNML!PetriNet (
			id <-  s.Name,
			pages <- Sequence{pp},
			type <- #GSPN
		),
		doc: PNML!PetriNetDoc (
			nets <- Sequence{net}
		),
		
		var : PNML!Variable (
			name <- 'Time'
		),
		varvals : PNML!VariableValues (
			variable <- var,
			values <- OrderedSet{}
		),
		study: PNML!Study (
			name <- 'DefaultStudy',
			vars <- Sequence{varvals}
		),
		evalList: PNML!EvaluationList (
			studies <- Sequence{study},
			measures <- PNML!Measure.allInstances()
		)
	do {
		for(i in IDM!InstantOfTime.allInstances()) {
			varvals.values <- varvals.values.append(i.timePoint);
		}
		for(i in IDM!IntervalOfTime.allInstances()) {
			varvals.values <- varvals.values.append(i.end);
		}
		for(i in IDM!IntervalOfTimeAveraged.allInstances()) {
			varvals.values <- varvals.values.append(i.end);
		}
	}
}

-- Crea la transizione di reset per ciascun componente
rule Component {
	from
		c : IDM!Component
	to
		doreset : PNML!Place
		(
			containerPage <- thisModule.getPage,
			id <- c.Name + '_doreset',
			initialMarking <- thisModule.newPTMarking(0)
		),
		reset : PNML!GSPNImmediateTransition
		(
			containerPage <- thisModule.getPage,
			id <- c.Name + '_reset',
			Priority <- thisModule.priReset,
			Weight <- 1.0,
			Guard <- thisModule.buildConditionNoExternalFaultsExcludingCoRepairs(c)
		),
		arcreset : PNML!GSPNArc
		(
			containerPage <- thisModule.getPage,
			id <- c.Name + '_arcreset',
			source <- doreset,
			target <- reset
		)
}

-- Crea le distribuzioni
rule Exponential { from e : IDM!Exponential to ee : PNML!Exponential ( Rate <- e.Rate ) }
rule Deterministic { 
	from 
		d : IDM!Deterministic ( d.Value > 0 )
	to 
		dd : PNML!Deterministic ( Value <- d.Value ) 
}
rule Uniform { from u : IDM!Uniform to uu : PNML!Uniform ( Lower <- u.Lower, Upper <- u.Upper ) }
rule Gaussian { from g : IDM!Gaussian to gg : PNML!Gaussian ( Mean <- g.Mean, Variance <- g.Variance ) }
rule Gamma { from g : IDM!Gamma to gg : PNML!Gamma ( Alpha <- g.Alpha, Beta <- g.Beta ) }
rule Weibull { from w : IDM!Weibull to ww : PNML!Weibull ( Alpha <- w.Alpha, Beta <- w.Beta ) }

-- Regole per InternalFault
abstract rule InternalFault {
	from 
		ft : IDM!InternalFault
	using {
		basename : String = ft.refImmediateComposite().Name + '_' + ft.Name;
		component_reset : PNML!GSPNTransition = ft.getResetTransition();
	}
	to
		--Place
		faulty : PNML!Place (
			containerPage <- thisModule.getPage,
			initialMarking <- thisModule.newPTMarking(0),
			id <- basename
		),
		transient : PNML!Place (
			containerPage <- thisModule.getPage,
			initialMarking <- thisModule.newPTMarking(0),
			id <- basename + '_transient'
		),
		tmpfaulty : PNML!Place (
			containerPage <- thisModule.getPage,
			initialMarking <- thisModule.newPTMarking(0),
			id <- basename + '_tmp'
		),
		
		e1 : PNML!OpEqual ( expression1 <- e2, expression2 <- e3 ),
		e2 : PNML!MarkingExpression ( place <- faulty ),
		e3 : PNML!ValueExpression ( value <- 0 ),
		
		--Transizioni (quelle per FO e TD vengono create dalle regole che estendono questa)
		casepermanent : PNML!GSPNImmediateTransition (
			containerPage <- thisModule.getPage,
			id <- basename + '_caseperm',
			Priority <- thisModule.priPropagationChoice,
			Weight <- ft.PermanentProbability
		),
		casetransient : PNML!GSPNImmediateTransition (
			containerPage <- thisModule.getPage,
			id <- basename + '_casetrans',
			Priority <- thisModule.priPropagationChoice,
			Weight <- (1 - ft.PermanentProbability)
		),		
		
		--Archi
		totmp : PNML!GSPNArc (
			containerPage <- thisModule.getPage,
			target <- tmpfaulty,
			id <- basename + '_totmp'
		),
			--Permanent Fault
		tmp_to_permcase : PNML!GSPNArc (
			containerPage <- thisModule.getPage,
			source <- tmpfaulty,
			target <- casepermanent,
			id <- basename + '_tmp_to_permcase'	
		),
		permcase_to_faulty : PNML!GSPNArc (
			containerPage <- thisModule.getPage,
			source <- casepermanent,
			target <- faulty,
			id <- basename + '_permcase_to_faulty'
		),
			--Transient Fault
		tmp_to_transcase : PNML!GSPNArc (
			containerPage <- thisModule.getPage,
			source <- tmpfaulty,
			target <- casetransient,
			id <- basename + '_tmp_to_transcase'	
		),
		transcase_to_faulty : PNML!GSPNArc (
			containerPage <- thisModule.getPage,
			source <- casetransient,
			target <- faulty,
			id <- basename + '_transcase_to_faulty'				
		),
		transcase_to_transient : PNML!GSPNArc (
			containerPage <- thisModule.getPage,
			source <- casetransient,
			target <- transient,
			id <- basename + '_transcase_to_transient'				
		),
		removetrans_trans : PNML!GSPNArc (
			containerPage <- thisModule.getPage,
			source <- transient,
			id <- basename + '_removetrans_trans'
		),
		removetrans_faulty : PNML!GSPNArc (
			containerPage <- thisModule.getPage,
			source <- faulty,
			id <- basename + '_removetrans_faulty'
		),

		--Arcs for component reset
		faulty_to_reset : PNML!GSPNArc (
			containerPage <- thisModule.getPage,
			source <- faulty,
			target <- component_reset,
			MultiplicityFunction <- thisModule.newMarkingExpression(faulty),
			id <- faulty_to_reset.defaultID()
		),
		transient_to_reset : PNML!GSPNArc (
			containerPage <- thisModule.getPage,
			source <- transient,
			target <- component_reset,
			MultiplicityFunction <- thisModule.newMarkingExpression(transient),
			id <- transient_to_reset.defaultID()
		),
		tmpfaulty_to_reset : PNML!GSPNArc (
			containerPage <- thisModule.getPage,
			source <- tmpfaulty,
			target <- component_reset,
			MultiplicityFunction <- thisModule.newMarkingExpression(tmpfaulty),
			id <- tmpfaulty_to_reset.defaultID()
		)
		
--		--Elements for firing only once
--		fireonce : PNML!Place (
--			containerPage <- thisModule.getPage,
--			initialMarking <- thisModule.newPTMarking(1),
--			id <- basename + '_fireonce'
--		),
--		fireonce_to_fo : PNML!GSPNArc (
--			containerPage <- thisModule.getPage,
--			source <- fireonce,
----			target <- ,
--			id <- basename + '_fireoncetofo'
--		)
}
rule InternalFaultTT extends InternalFault { --FO timed, TD timed
	from 
		ft : IDM!InternalFault
		(
			if ft.Occurrence.oclIsTypeOf(IDM!Deterministic) then
				if ft.TransientDuration.oclIsTypeOf(IDM!Deterministic) then
					ft.Occurrence.Value > 0 and ft.TransientDuration.Value > 0
				else
					ft.Occurrence.Value > 0
				endif
			else
				if ft.TransientDuration.oclIsTypeOf(IDM!Deterministic) then
					ft.TransientDuration.Value > 0
				else
					true
				endif
			endif
		)
	to
		faulty : PNML!Place,
		tmpfaulty : PNML!Place,
		e1 : PNML!OpEqual ( expression1 <- e2, expression2 <- e3 ),
		fo : PNML!GSPNTimedTransition
		(
			containerPage <- thisModule.getPage,
			Distribution <- ft.Occurrence,
			id <- ft.Name + '_FO',
			Guard <- e1
		),
		td : PNML!GSPNTimedTransition
		(
			containerPage <- thisModule.getPage,
			Distribution <- ft.TransientDuration,
			id <- ft.Name + '_TD'
		),
		totmp : PNML!GSPNArc ( source <- fo ),
		removetrans_trans : PNML!GSPNArc ( target <- td ),
		removetrans_faulty : PNML!GSPNArc ( target <- td )
--		fireonce_to_fo : PNML!GSPNArc ( target <- fo )
}
rule InternalFaultII extends InternalFault { --FO immediate, TD immediate
	from 
		ft : IDM!InternalFault
		(
			if ft.Occurrence.oclIsTypeOf(IDM!Deterministic) and ft.TransientDuration.oclIsTypeOf(IDM!Deterministic) then
				ft.Occurrence.Value = 0 and ft.TransientDuration.Value = 0
			else
				false
			endif
		)
	to
		faulty : PNML!Place,
		tmpfaulty : PNML!Place,
		fo : PNML!GSPNImmediateTransition
		(
			containerPage <- thisModule.getPage,
			id <- ft.Name + '_FO',
			Priority <- thisModule.priPropagation,
			Weight <- 1.0,
			Guard <- e1
		),
		td : PNML!GSPNImmediateTransition
		(
			containerPage <- thisModule.getPage,
			id <- ft.Name + '_TD',
			Priority <- thisModule.priTransientDuration,
			Weight <- 1.0
		),
		totmp : PNML!GSPNArc ( source <- fo ),
		removetrans_trans : PNML!GSPNArc ( target <- td ),
		removetrans_faulty : PNML!GSPNArc ( target <- td )
--		fireonce_to_fo : PNML!GSPNArc ( target <- fo )
}
rule InternalFaultTI extends InternalFault { --FO timed, TD immediate
	from
		ft : IDM!InternalFault
		(
			if ft.Occurrence.oclIsTypeOf(IDM!Deterministic) then
				if ft.TransientDuration.oclIsTypeOf(IDM!Deterministic) then
					ft.Occurrence.Value > 0 and ft.TransientDuration.Value = 0
				else
					false
				endif
			else
				if ft.TransientDuration.oclIsTypeOf(IDM!Deterministic) then
					ft.TransientDuration.Value = 0
				else
					false
				endif
			endif
		)
	to
		faulty : PNML!Place,
		tmpfaulty : PNML!Place,
		e1 : PNML!OpEqual ( expression1 <- e2, expression2 <- e3 ),
		fo : PNML!GSPNTimedTransition
		(
			containerPage <- thisModule.getPage,
			Distribution <- ft.Occurrence,
			id <- ft.Name + '_FO',
			Guard <- e1
		),
		td : PNML!GSPNImmediateTransition
		(
			containerPage <- thisModule.getPage,
			id <- ft.Name + '_TD',
			Priority <- thisModule.priTransientDuration,
			Weight <- 1.0
		),
		totmp : PNML!GSPNArc ( source <- fo ),
		removetrans_trans : PNML!GSPNArc ( target <- td ),
		removetrans_faulty : PNML!GSPNArc ( target <- td )
--		fireonce_to_fo : PNML!GSPNArc ( target <- fo )
}
rule InternalFaultIT extends InternalFault { --FO immediate, TD timed
	from 
		ft : IDM!InternalFault
		(
			if ft.Occurrence.oclIsTypeOf(IDM!Deterministic) then
				if ft.TransientDuration.oclIsTypeOf(IDM!Deterministic) then
					ft.Occurrence.Value = 0 and ft.TransientDuration.Value > 0
				else
					ft.Occurrence.Value = 0
				endif
			else
				false
			endif
		)
	to
		faulty : PNML!Place,
		tmpfaulty : PNML!Place,
		e1 : PNML!OpEqual ( expression1 <- e2, expression2 <- e3 ),
		fo : PNML!GSPNImmediateTransition
		(
			containerPage <- thisModule.getPage,
			id <- ft.Name + '_FO',
			Priority <- thisModule.priPropagation,
			Weight <- 1.0,
			Guard <- e1
		),
		td : PNML!GSPNTimedTransition
		(
			containerPage <- thisModule.getPage,
			Distribution <- ft.TransientDuration,
			id <- ft.Name + '_TD'
		),
		totmp : PNML!GSPNArc ( source <- fo ),
		removetrans_trans : PNML!GSPNArc ( target <- td ),
		removetrans_faulty : PNML!GSPNArc ( target <- td )
--		fireonce_to_fo : PNML!GSPNArc ( target <- fo )
}

rule Error { --manca l'implementazione di VanishingTime 
	from 
		e : IDM!Error
	using {
		basename : String = e.refImmediateComposite().Name + '_' + e.Name;
		component_reset : PNML!GSPNTransition = e.getResetTransition();
	}
	to
		err : PNML!Place (
			id <- basename,
			containerPage <- thisModule.getPage,
			initialMarking <- thisModule.newPTMarking(0)
		),
		detected : PNML!Place (
			id <- basename + '_detected',
			containerPage <- thisModule.getPage,
			initialMarking <- thisModule.newPTMarking(0)
		),
		--Arcs for component reset
		err_to_reset : PNML!GSPNArc (
			containerPage <- thisModule.getPage,
			source <- err,
			target <- component_reset,
			MultiplicityFunction <- thisModule.newMarkingExpression(err),
			id <- err_to_reset.defaultID()
		),
		detected_to_reset : PNML!GSPNArc (
			containerPage <- thisModule.getPage,
			source <- detected,
			target <- component_reset,
			MultiplicityFunction <- thisModule.newMarkingExpression(detected),
			id <- detected_to_reset.defaultID()
		)
}
rule ErrorVanishImmediate extends Error {
	from
		e : IDM!Error
		(
			if e.VanishingTime.oclIsUndefined() then
				false
			else
				if e.VanishingTime.oclIsTypeOf(IDM!Deterministic) then
					e.VanishingTime.Value = 0
				else
					false
				endif
			endif
		)
	to
		err : PNML!Place,
		detected : PNML!Place,
		vanish : PNML!GSPNImmediateTransition
		(
			containerPage <- thisModule.getPage,
			id <- basename + '_vanish',
			Priority <- thisModule.priTransientDuration,
			Weight <- 1.0
		),
		tovanish : PNML!GSPNArc
		(
			containerPage <- thisModule.getPage,
			id <- basename + '_to_vanish',
			source <- err,
			target <- vanish
		)
}
rule ErrorVanishTimed extends Error {
	from
		e : IDM!Error
		(
			if e.VanishingTime.oclIsUndefined() then
				false
			else
				if e.VanishingTime.oclIsTypeOf(IDM!Deterministic) then
					e.VanishingTime.Value > 0
				else
					true
				endif
			endif
		)
	to
		err : PNML!Place,
		detected : PNML!Place,
		vanish : PNML!GSPNTimedTransition
		(
			containerPage <- thisModule.getPage,
			id <- basename + '_vanish',
			Distribution <- e.VanishingTime
		),
		tovanish : PNML!GSPNArc
		(
			containerPage <- thisModule.getPage,
			id <- basename + '_to_vanish',
			source <- err,
			target <- vanish
		)
}
rule ErrorEPFChoice(e : IDM!Error, epf : IDM!ErrorsProducesFailures) {
	to
		epfSelected : PNML!Place
		(
			id <- e.Name + '_sel_' + epf.Name,
			containerPage <- thisModule.getPage,
			initialMarking <- thisModule.newPTMarking(0)
		),
		trSelection : PNML!GSPNImmediateTransition
		(
			id <- e.Name + '_choice_' + epf.Name,
			containerPage <- thisModule.getPage,
			Weight <- epf.Weight,
			Priority <- thisModule.priPropagationChoice,
			Guard <- thisModule.CreateEPFGuard(epf)
		),
		tr_to_selected : PNML!GSPNArc 
		(
			containerPage <- thisModule.getPage,
			source <- trSelection,
			target <- epfSelected,
			id <- trSelection.id + '_to_sel'
		),
		tr_to_selected_inh : PNML!GSPNArc 
		(
			containerPage <- thisModule.getPage,
			source <- epfSelected,
			target <- trSelection,
			type <- #inhibitor,
			id <- trSelection.id + '_to_sel_inh'
		)
	do {
--		'ErrorEPFChoice'.debug();
		epfSelected;
	}
}
rule ErrorIPChoice(e : IDM!Error, iprop : IDM!InternalPropagation) {
	to
		ipSelected : PNML!Place
		(
			id <- e.Name + '_sel_' + iprop.Name,
			containerPage <- thisModule.getPage,
			initialMarking <- thisModule.newPTMarking(0)
		),
		trSelection : PNML!GSPNImmediateTransition
		(
			id <- e.Name + '_choice_' + iprop.Name,
			containerPage <- thisModule.getPage,
			Weight <- iprop.Weight,
			Priority <- thisModule.priPropagationChoice,
--			Guard <- PNML!OpFalse.newInstance()
			Guard <- thisModule.CreateIPGuard(iprop)
		),
		tr_to_selected : PNML!GSPNArc 
		(
			containerPage <- thisModule.getPage,
			source <- trSelection,
			target <- ipSelected,
			id <- trSelection.id + '_to_sel'
		),
		tr_to_selected_inh : PNML!GSPNArc 
		(
			containerPage <- thisModule.getPage,
			source <- ipSelected,
			target <- trSelection,
			type <- #inhibitor,
			id <- trSelection.id + '_to_sel_inh'
		)
	do {
--		'ErrorIPChoice'.debug();
		ipSelected;
	}
}

rule FailureMode {
	from
		fm : IDM!FailureMode
	using{
		component_reset : PNML!GSPNTransition = fm.getResetTransition();
	}
	to
		fmode : PNML!Place (
			id <- fm.refImmediateComposite().Name + '_' + fm.Name,
			containerPage <- thisModule.getPage,
			initialMarking <- thisModule.newPTMarking(0)			
		),
		fmode_to_reset : PNML!GSPNArc (
			containerPage <- thisModule.getPage,
			source <- fmode,
			target <- component_reset,
			MultiplicityFunction <- thisModule.newMarkingExpression(fmode),
			id <- fmode_to_reset.defaultID()
		)
}

--FaultsExpression elements
rule FaultsExpressionNode(n : IDM!FaultsExpressionFaultNode) {
	using {
		out : PNML!LogicalExpression = OclUndefined;
	}
	do {
		if(n.oclIsTypeOf(IDM!FaultsExpressionFaultNode)) {
			out <- thisModule.FaultsExpressionFaultNode(n);
		}else if(n.oclIsTypeOf(IDM!FaultsExpressionAndNode)) {
			out <- thisModule.FaultsExpressionAndNode(n);
		}else if(n.oclIsTypeOf(IDM!FaultsExpressionOrNode)) {
			out <- thisModule.FaultsExpressionOrNode(n);
		}else if(n.oclIsTypeOf(IDM!FaultsExpressionNotNode)) {
			out <- thisModule.FaultsExpressionNotNode(n);
		}

		out;
	}
}

rule FaultsExpressionFaultNode(n : IDM!FaultsExpressionFaultNode) {
	to
		nn : PNML!OpGreater ( expression1 <- e1, expression2 <- e2 ),
		e1 : PNML!MarkingExpression (
			place <- 
			if n.Fault.oclIsTypeOf(IDM!InternalFault) then
				n.Fault
			else
				n.Fault.Source
			endif
		),
		e2 : PNML!ValueExpression ( value <- 0 )
	do {
		nn;	
	}
}
rule FaultsExpressionNotNode(n : IDM!FaultsExpressionNotNode) {
	to
		nn : PNML!OpNot (
			expression <- thisModule.FaultsExpressionNode(n.FaultsExpression)
		)
	do {
		nn;	
	}
}
rule FaultsExpressionAndNode(n : IDM!FaultsExpressionAndNode) {
	to
		nn : PNML!OpAnd (
			expression1 <- thisModule.FaultsExpressionNode(n.FaultsExpression1),
			expression2 <- thisModule.FaultsExpressionNode(n.FaultsExpression2)
		)
	do {
		nn;	
	}
}
rule FaultsExpressionOrNode(n : IDM!FaultsExpressionOrNode) {
	to
		nn : PNML!OpOr ( 
			expression1 <- thisModule.FaultsExpressionNode(n.FaultsExpression1), 
			expression2 <- thisModule.FaultsExpressionNode(n.FaultsExpression2)
		)
	do {
		nn;
	}
}

--ErrorsExpression elements
rule ErrorsExpressionNode(n : IDM!ErrorsExpressionNode) {
	using {
		out : PNML!LogicalExpression = OclUndefined;
	}
	do {
		if(n.oclIsTypeOf(IDM!ErrorsExpressionErrorNode)) {
			out <- thisModule.ErrorsExpressionErrorNode(n);
		}else if(n.oclIsTypeOf(IDM!ErrorsExpressionAndNode)) {
			out <- thisModule.ErrorsExpressionAndNode(n);
		}else if(n.oclIsTypeOf(IDM!ErrorsExpressionOrNode)) {
			out <- thisModule.ErrorsExpressionOrNode(n);
		}else if(n.oclIsTypeOf(IDM!ErrorsExpressionNotNode)) {
			out <- thisModule.ErrorsExpressionNotNode(n);
		}

		out;
	}
}

rule ErrorsExpressionErrorNode(n : IDM!ErrorsExpressionErrorNode) {
	to
		nn : PNML!OpGreater ( expression1 <- e1, expression2 <- e2 ),
		e1 : PNML!MarkingExpression
		(
			place <- n.Error
		),
		e2 : PNML!ValueExpression ( value <- 0 )
	do {
		nn;
	}
}
rule ErrorsExpressionNotNode(n : IDM!ErrorsExpressionNotNode) {
	to
		nn : PNML!OpNot ( 
			expression <- 
				thisModule.ErrorsExpressionNode(n.ErrorsExpression)
		)
	do {
		nn;
	}
}
rule ErrorsExpressionAndNode(n : IDM!ErrorsExpressionAndNode) {
	to
		nn : PNML!OpAnd (
			e1 <- thisModule.ErrorsExpressionNode(n.ErrorsExpression1),
			e2 <- thisModule.ErrorsExpressionNode(n.ErrorsExpression2)
		)
	do {
		nn;
	}
}
rule ErrorsExpressionOrNode(n : IDM!ErrorsExpressionOrNode) {
	to
		nn : PNML!OpOr (
			e1 <- thisModule.ErrorsExpressionNode(n.ErrorsExpression1),
			e2 <- thisModule.ErrorsExpressionNode(n.ErrorsExpression2)
		)
	do {
		nn;
	}
}

--FaultsGenerateErrors
abstract rule FGE {
	from
		fge : IDM!FaultsGenerateErrors
	using {
		basename : String = fge.refImmediateComposite().Name + '_' + fge.Name;
	}
	to
		andop : PNML!OpAnd
		(
			expression1 <- thisModule.newOpAnd(thisModule.FaultsExpressionNode(fge.PropagationLogic),
											   thisModule.newOpAnd(
											       thisModule.newOpEqual(
											           thisModule.newMarkingExpression(tmp),
													   thisModule.newValueExpression(0)
												   ),
											       thisModule.buildConditionComponentIsNotFailed(fge.Component)
											   ))
		),		
		tmp : PNML!Place
		(
			id <- basename + '_tmp',
			initialMarking <- thisModule.newPTMarking(0),
			containerPage <- thisModule.getPage
		),
		casepropagate : PNML!GSPNImmediateTransition
		(
			id <- basename + '_caseprop',
--			Weight <- fge.PropagationProbability * fge.Weight,	--This is a workaround!
			Weight <- fge.Weight,
			Priority <- thisModule.priPropagationChoice,
			containerPage <- thisModule.getPage
		),
		caseskip : PNML!GSPNImmediateTransition
		(
			id <- basename + '_caseskip',
			Weight <- ( 1 - casepropagate.Weight ),
			Priority <- thisModule.priPropagationChoice,
			containerPage <- thisModule.getPage,
			Guard <- PNML!OpFalse.newInstance()		--This is a workaround!
		),
		blocker : PNML!Place
		(
			id <- basename + '_blocker',
			initialMarking <- thisModule.newPTMarking(0),
			containerPage <- thisModule.getPage
		),
		--Archi
		totmp : PNML!GSPNArc
		(
			id <- basename + '_totmp',
--			source <- trfge,
			target <- tmp,
			containerPage <- thisModule.getPage
		),
		topropagate : PNML!GSPNArc
		(
			id <- basename + '_toprop',
			containerPage <- thisModule.getPage,
			source <- tmp,
			target <- casepropagate
		),
		toskip : PNML!GSPNArc
		(
			id <- basename + '_toskip',
			containerPage <- thisModule.getPage,
			source <- tmp,
			target <- caseskip
		),
		toblocker : PNML!GSPNArc
		(
			id <- basename + '_toblocker',
			containerPage <- thisModule.getPage,
			--source <- trfge,
			target <- blocker
		),
		toblocker_inhibit : PNML!GSPNArc
		(
			id <- basename + '_toblocker_inhibit',
			containerPage <- thisModule.getPage,
			source <- blocker,
			--target <- trfge,
			type <- #inhibitor
		),
		--Arcs for component reset
		tmp_to_reset : PNML!GSPNArc
		(
			containerPage <- thisModule.getPage,
			source <- tmp,
			target <- fge.refImmediateComposite().getResetTransition(),
			MultiplicityFunction <- thisModule.newMarkingExpression(tmp),
			id <- tmp_to_reset.defaultID()
		),
		blocker_to_reset : PNML!GSPNArc
		(
			containerPage <- thisModule.getPage,
			source <- blocker,
			target <- fge.refImmediateComposite().getResetTransition(),
			MultiplicityFunction <- thisModule.newMarkingExpression(blocker),
			id <- blocker_to_reset.defaultID()
		)
--		--Elements for firing only once
--		fireonce : PNML!Place (
--			containerPage <- thisModule.getPage,
--			initialMarking <- thisModule.newPTMarking(1),
--			id <- basename + '_fireonce'
--		),
--		fireonce_to_trfge : PNML!GSPNArc (
--			containerPage <- thisModule.getPage,
--			source <- fireonce,
----			target <- ,
--			id <- basename + '_fireoncetofo'
--		)
}
rule FGETimed extends FGE {
	from
		fge : IDM!FaultsGenerateErrors
		(
			if fge.ActivationDelay.oclIsTypeOf(IDM!Deterministic) then
				fge.ActivationDelay.Value > 0
			else
				true
			endif
		)
	to
		trfge : PNML!GSPNTimedTransition
		(
			id <- basename,
			Distribution <- fge.ActivationDelay,
			containerPage <- thisModule.getPage,
			Guard <- andop
		),
		andop : PNML!OpAnd,
		totmp : PNML!GSPNArc ( source <- trfge ),
		toblocker : PNML!GSPNArc ( source <- trfge ),
		toblocker_inhibit : PNML!GSPNArc ( target <- trfge )
--		fireonce_to_trfge : PNML!GSPNArc ( target <- trfge )
	do {
		thisModule.tmpLogicExp <- andop;

		for(e in fge.Destination.subSequence(2, fge.Destination.size())) {
			thisModule.tmpLogicExp.expression2 <- thisModule.newOpOr( 
				thisModule.newOpEqual(
					thisModule.newMarkingExpression(e),
					thisModule.newValueExpression(0)
				),
				OclUndefined
			);
			thisModule.newOutputArc(casepropagate, e);
			thisModule.tmpLogicExp <- thisModule.tmpLogicExp.expression2;
		}
		
		thisModule.tmpLogicExp.expression2 <- thisModule.newOpEqual(
			thisModule.newMarkingExpression(fge.Destination.first()),
			thisModule.newValueExpression(0)
		);
		thisModule.newOutputArc(casepropagate, fge.Destination.first());
		thisModule.tmpLogicExp <- thisModule.tmpLogicExp.expression2;
	}
}
rule FGEImmediate extends FGE {
	from
		fge : IDM!FaultsGenerateErrors
		(
			if fge.ActivationDelay.oclIsTypeOf(IDM!Deterministic) then
				fge.ActivationDelay.Value = 0
			else
				false
			endif
		)
	to
		trfge : PNML!GSPNImmediateTransition
		(
			id <- basename,
			containerPage <- thisModule.getPage,
			Weight <- fge.Weight,
			Priority <- thisModule.priPropagation,
			Guard <- andop
		),
		andop : PNML!OpAnd,
		totmp : PNML!GSPNArc ( source <- trfge ),
		toblocker : PNML!GSPNArc ( source <- trfge ),
		toblocker_inhibit : PNML!GSPNArc ( target <- trfge )
--		fireonce_to_trfge : PNML!GSPNArc ( target <- trfge )
	do {
	
		thisModule.tmpLogicExp <- andop;

		for(e in fge.Destination.subSequence(2, fge.Destination.size())) {
			thisModule.tmpLogicExp.expression2 <- thisModule.newOpOr( 
				thisModule.newOpEqual(
					thisModule.newMarkingExpression(e),
					thisModule.newValueExpression(0)
				),
				OclUndefined
			);
			thisModule.newOutputArc(casepropagate, e);
			thisModule.tmpLogicExp <- thisModule.tmpLogicExp.expression2;
		}
		
		thisModule.tmpLogicExp.expression2 <- thisModule.newOpEqual(
			thisModule.newMarkingExpression(fge.Destination.first()),
			thisModule.newValueExpression(0)
		);
		thisModule.newOutputArc(casepropagate, fge.Destination.first());
		thisModule.tmpLogicExp <- thisModule.tmpLogicExp.expression2;
	}
}

--ErrorsProduceFailures
abstract rule EPF {
	from
		epf : IDM!ErrorsProducesFailures
	using {
		basename : String = epf.refImmediateComposite().Name + '_' + epf.Name;
	}
	to
		tmp : PNML!Place
		(
			id <- basename + '_tmp',
			initialMarking <- thisModule.newPTMarking(0),
			containerPage <- thisModule.getPage
		),
		casepropagate : PNML!GSPNImmediateTransition
		(
			id <- basename + '_caseprop',
			Weight <- epf.PropagationProbability,
			Priority <- thisModule.priPropagationChoice,
			containerPage <- thisModule.getPage
		),
		caseskip : PNML!GSPNImmediateTransition
		(
			id <- basename + '_caseskip',
			Weight <- ( 1 - epf.PropagationProbability ),
			Priority <- thisModule.priPropagationChoice,
			containerPage <- thisModule.getPage
		),
		blocker : PNML!Place
		(
			id <- basename + '_blocker',
			initialMarking <- thisModule.newPTMarking(0),
			containerPage <- thisModule.getPage
		),
		--Archi
		totmp : PNML!GSPNArc
		(
			id <- basename + '_totmp',
--			source <- trfge,
			target <- tmp,
			containerPage <- thisModule.getPage
		),
		topropagate : PNML!GSPNArc
		(
			id <- basename + '_toprop',
			containerPage <- thisModule.getPage,
			source <- tmp,
			target <- casepropagate
		),
		toskip : PNML!GSPNArc
		(
			id <- basename + '_toskip',
			containerPage <- thisModule.getPage,
			source <- tmp,
			target <- caseskip
		),
		toblocker : PNML!GSPNArc
		(
			id <- basename + '_toblocker',
			containerPage <- thisModule.getPage,
			--source <- trepf,
			target <- blocker
		),
		toblocker_inhibit : PNML!GSPNArc
		(
			id <- basename + '_toblocker_inhibit',
			containerPage <- thisModule.getPage,
			source <- blocker,
			--target <- trepf,
			type <- #inhibitor
		),
		--Arcs for component reset
		tmp_to_reset : PNML!GSPNArc
		(
			containerPage <- thisModule.getPage,
			source <- tmp,
			target <- epf.refImmediateComposite().getResetTransition(),
			MultiplicityFunction <- thisModule.newMarkingExpression(tmp),
			id <- tmp_to_reset.defaultID()
		),
		blocker_to_reset : PNML!GSPNArc
		(
			containerPage <- thisModule.getPage,
			source <- blocker,
			target <- epf.refImmediateComposite().getResetTransition(),
			MultiplicityFunction <- thisModule.newMarkingExpression(blocker),
			id <- blocker_to_reset.defaultID()
		)
}
rule EPFTimed extends EPF {
	from
		epf : IDM!ErrorsProducesFailures
		(
			if epf.PropagationDelay.oclIsTypeOf(IDM!Deterministic) then
				epf.PropagationDelay.Value > 0
			else
				true
			endif
		)
	to
		trepf : PNML!GSPNTimedTransition
		(
			id <- basename,
			Distribution <- epf.PropagationDelay,
			containerPage <- thisModule.getPage
		),
		totmp : PNML!GSPNArc ( source <- trepf ),
		toblocker : PNML!GSPNArc ( source <- trepf ),
		toblocker_inhibit : PNML!GSPNArc ( target <- trepf )
	do {
		for(fm in epf.Destination) {
			thisModule.newOutputArc(casepropagate, fm);
		}
		
		trepf.Guard <- thisModule.CreateEPFGuard(epf);
		thisModule.EPFFinalizeChoice(epf);
	}
}
rule EPFImmediate extends EPF {
	from
		epf : IDM!ErrorsProducesFailures
		(
			if epf.PropagationDelay.oclIsTypeOf(IDM!Deterministic) then
				epf.PropagationDelay.Value = 0
			else
				false
			endif
		)
	to
		trepf : PNML!GSPNImmediateTransition
		(
			id <- basename,
			containerPage <- thisModule.getPage,
			Weight <- epf.Weight,
			Priority <- thisModule.priPropagation
		),
		totmp : PNML!GSPNArc ( source <- trepf ),
		toblocker : PNML!GSPNArc ( source <- trepf ),
		toblocker_inhibit : PNML!GSPNArc ( target <- trepf )
	do {
--		'EPFImmediate'.debug();
		for(fm in epf.Destination) {
			thisModule.newOutputArc(casepropagate, fm);
		}
		
		trepf.Guard <- thisModule.CreateEPFGuard(epf);
		thisModule.EPFFinalizeChoice(epf);
	}
}
rule CreateEPFGuard(epf : IDM!ErrorsProducesFailures) {
	using {
		tmpLogicExp : PNML!LogicalExpression = OclUndefined;
		andop : PNML!OpAnd = OclUndefined;
	}
	do {
		andop <- thisModule.newOpAnd (
					thisModule.newOpAnd(
							thisModule.ErrorsExpressionNode(epf.PropagationLogic),
							thisModule.newOpAnd(
								thisModule.newOpEqual(
						            thisModule.newMarkingExpression(
						           		thisModule.resolveTemp(epf, 'tmp')
								    ),
									thisModule.newValueExpression(0)
								),
								thisModule.buildConditionComponentIsNotFailed(epf.Component)
							)
					),			   
					OclUndefined
				);		
		
		tmpLogicExp <- andop;

		for(fm in epf.Destination.subSequence(2, epf.Destination.size())) {
			tmpLogicExp.expression2 <- thisModule.newOpOr( 
				thisModule.newOpEqual(
					thisModule.newMarkingExpression(fm),
					thisModule.newValueExpression(0)
				),
				OclUndefined
			);
			tmpLogicExp <- tmpLogicExp.expression2;
		}
		
		tmpLogicExp.expression2 <- thisModule.newOpEqual(
			thisModule.newMarkingExpression(epf.Destination.first()),
			thisModule.newValueExpression(0)
		);
		
		andop;
	}
}
rule EPFFinalizeChoice(epf : IDM!ErrorsProducesFailures) {
	using {
		tmpArc : PNML!GSPNArc = OclUndefined;
		selPlace : PNML!Place = OclUndefined;
	}
	do {
		for(e in epf.Source) {
			selPlace <- thisModule.ErrorEPFChoice(e, epf);
			thisModule.newOutputArc(selPlace, thisModule.resolveTemp(epf, 'trepf'));
		}
	}
}

--InternalPropagation
abstract rule InternalPropagation {
	from
		iprop : IDM!InternalPropagation
	using {
		basename : String = iprop.refImmediateComposite().Name + '_' + iprop.Name;
	}
	to
		tmp : PNML!Place
		(
			id <- basename + '_tmp',
			initialMarking <- thisModule.newPTMarking(0),
			containerPage <- thisModule.getPage
		),
		casepropagate : PNML!GSPNImmediateTransition
		(
			id <- basename + '_caseprop',
--			Weight <- iprop.PropagationProbability * iprop.Weight,	--This is a workaround!
			Weight <- iprop.PropagationProbability,
			Priority <- thisModule.priPropagationChoice,
			containerPage <- thisModule.getPage
		),
		caseskip : PNML!GSPNImmediateTransition
		(
			id <- basename + '_caseskip',
			Weight <- ( 1 - casepropagate.Weight ),
--			Weight <- '1.0E-6'.toReal(),
			Priority <- thisModule.priPropagationChoice,
			containerPage <- thisModule.getPage,
			Guard <- PNML!OpFalse.newInstance()		--This is a workaround!
		),
		blocker : PNML!Place
		(
			id <- basename + '_blocker',
			initialMarking <- thisModule.newPTMarking(0),
			containerPage <- thisModule.getPage
		),
		--Archi
		totmp : PNML!GSPNArc
		(
			id <- basename + '_totmp',
--			source <- trfge,
			target <- tmp,
			containerPage <- thisModule.getPage
		),
		topropagate : PNML!GSPNArc
		(
			id <- basename + '_toprop',
			containerPage <- thisModule.getPage,
			source <- tmp,
			target <- casepropagate
		),
		toskip : PNML!GSPNArc
		(
			id <- basename + '_toskip',
			containerPage <- thisModule.getPage,
			source <- tmp,
			target <- caseskip
		),
		toblocker : PNML!GSPNArc
		(
			id <- basename + '_toblocker',
			containerPage <- thisModule.getPage,
			--source <- trepf,
			target <- blocker
		),
		toblocker_inhibit : PNML!GSPNArc
		(
			id <- basename + '_toblocker_inhibit',
			containerPage <- thisModule.getPage,
			source <- blocker,
			--target <- trepf,
			type <- #inhibitor
		),
		--Arcs for component reset
		tmp_to_reset : PNML!GSPNArc
		(
			containerPage <- thisModule.getPage,
			source <- tmp,
			target <- iprop.refImmediateComposite().getResetTransition(),
			MultiplicityFunction <- thisModule.newMarkingExpression(tmp),
			id <- tmp_to_reset.defaultID()
		),
		blocker_to_reset : PNML!GSPNArc
		(
			containerPage <- thisModule.getPage,
			source <- blocker,
			target <- iprop.refImmediateComposite().getResetTransition(),
			MultiplicityFunction <- thisModule.newMarkingExpression(blocker),
			id <- blocker_to_reset.defaultID()
		)
}
rule InternalPropagationTimed extends InternalPropagation {
	from
		iprop : IDM!InternalPropagation
		(
			if iprop.PropagationDelay.oclIsTypeOf(IDM!Deterministic) then
				iprop.PropagationDelay.Value > 0
			else
				true
			endif
		)
	to
		triprop : PNML!GSPNTimedTransition
		(
			id <- basename,
			Distribution <- iprop.PropagationDelay,
			containerPage <- thisModule.getPage
		),
		totmp : PNML!GSPNArc ( source <- triprop ),
		toblocker : PNML!GSPNArc ( source <- triprop ),
		toblocker_inhibit : PNML!GSPNArc ( target <- triprop )
	do {
		for(e in iprop.Destination) {
			thisModule.newOutputArc(casepropagate, e);
		}
		triprop.Guard <- thisModule.CreateIPGuard(iprop);
		thisModule.IPFinalizeChoice(iprop);
	}
}
rule InternalPropagationImmediate extends InternalPropagation {
	from
		iprop : IDM!InternalPropagation
		(
			if iprop.PropagationDelay.oclIsTypeOf(IDM!Deterministic) then
				iprop.PropagationDelay.Value = 0
			else
				false
			endif
		)
	to
		triprop : PNML!GSPNImmediateTransition
		(
			id <- basename,
			Weight <- iprop.Weight,
			Priority <- thisModule.priPropagation,
			containerPage <- thisModule.getPage
		),
		totmp : PNML!GSPNArc ( source <- triprop ),
		toblocker : PNML!GSPNArc ( source <- triprop ),
		toblocker_inhibit : PNML!GSPNArc ( target <- triprop )
	do {
--		'InternalPropagationImmediate'.debug();

		for(e in iprop.Destination) {
			thisModule.newOutputArc(casepropagate, e);
		}
		triprop.Guard <- thisModule.CreateIPGuard(iprop);
		thisModule.IPFinalizeChoice(iprop);
	}
}
rule CreateIPGuard(iprop : IDM!InternalPropagation) {
	using {
		tmpLogicExp : PNML!LogicalExpression = OclUndefined;
		andop : PNML!OpAnd = OclUndefined;
	}
	do {
--		'CreateIPGuard'.debug();
		andop <- thisModule.newOpAnd( 
			if(not iprop.FaultGuard.oclIsUndefined()) then
				thisModule.newOpAnd(
					thisModule.FaultsExpressionNode(iprop.FaultGuard),
					thisModule.newOpAnd(thisModule.ErrorsExpressionNode(iprop.PropagationLogic),
													   thisModule.newOpAnd(
													       thisModule.newOpEqual(
													           thisModule.newMarkingExpression(
													           		thisModule.resolveTemp(iprop, 'tmp')
													           ),
															   thisModule.newValueExpression(0)
														   ),
													       thisModule.buildConditionComponentIsNotFailed(iprop.Component)
													   ))
				)
			else			
				thisModule.newOpAnd(thisModule.ErrorsExpressionNode(iprop.PropagationLogic),
												   thisModule.newOpAnd(
												       thisModule.newOpEqual(
												           thisModule.newMarkingExpression(
												           		thisModule.resolveTemp(iprop, 'tmp')
												           ),
														   thisModule.newValueExpression(0)
													   ),
												       thisModule.buildConditionComponentIsNotFailed(iprop.Component)
												   ))
			endif,
			OclUndefined
		);
		
		tmpLogicExp <- andop;

		for(e in iprop.Destination.subSequence(2, iprop.Destination.size())) {
			tmpLogicExp.expression2 <- thisModule.newOpOr( 
				thisModule.newOpEqual(
					thisModule.newMarkingExpression(e),
					thisModule.newValueExpression(0)
				),
				OclUndefined
			);
			tmpLogicExp <- tmpLogicExp.expression2;
		}
		
		tmpLogicExp.expression2 <- thisModule.newOpEqual(
			thisModule.newMarkingExpression(iprop.Destination.first()),
			thisModule.newValueExpression(0)
		);
	
		andop;
	}
}
rule IPFinalizeChoice(iprop : IDM!InternalPropagation) {
	using {
		tmpArc : PNML!GSPNArc = OclUndefined;
		selPlace : PNML!Place = OclUndefined;
	}
	do {
		for(e in iprop.Source) {
			selPlace <- thisModule.ErrorIPChoice(e, iprop);
			thisModule.newOutputArc(selPlace, thisModule.resolveTemp(iprop, 'triprop'));
		}
	}
}

-- ScheduleExpression nodes
	-- T
rule ScheduleExpImmediately {
	from
		se : IDM!ScheduleExpressionImmediately
	using {
		act : IDM!Activity = IDM!Activity.allInstances()->select(i | i.When.T = se).first();
	}
	to
		tr : PNML!GSPNImmediateTransition
		(
			containerPage <- thisModule.getPage,
			id <- act.Name + '_schedule_T',
			Weight <- 1.0,
			Priority <- thisModule.priActivitySchedule,
			Guard <- g_and
		),
		arc : PNML!GSPNArc
		(
			containerPage <- thisModule.getPage,
			id <- act.Name + '_schedule_T_oarc',
			source <- tr,
			target <- act
		),
		g_and : PNML!OpAnd
		(
			expression1 <- act.When.EX,
			expression2 <- g_eq
		),
		g_eq : PNML!OpEqual
		(
			expression1 <- g_mexp,
			expression2 <- thisModule.newValueExpression(0)
		),
		g_mexp : PNML!MarkingExpression
		(
			place <- act
		)
}
rule ScheduleExpAtTime {
	from 
		se : IDM!ScheduleExpressionAtTime
	using {
		act : IDM!Activity = IDM!Activity.allInstances()->select(i | i.When.T = se).first();
	}
	to
		tr : PNML!GSPNTimedTransition
		(
			containerPage <- thisModule.getPage,
			id <- act.Name + '_schedule_T',
			Distribution <- delay
		),
		arc : PNML!GSPNArc
		(
			containerPage <- thisModule.getPage,
			id <- act.Name + '_schedule_T_oarc',
			source <- tr,
			target <- act
		),
		delay : PNML!Deterministic ( Value <- se.t ),
		wait : PNML!Place
		(
			containerPage <- thisModule.getPage,
			id <- act.Name + '_schedule_T_wait',
			initialMarking <- thisModule.newPTMarking(1)
		),
		fromwait : PNML!GSPNArc
		(
			containerPage <- thisModule.getPage,
			id <- act.Name + '_schedule_T_fromwait',
			source <- wait,
			target <- tr
		)
}
rule ScheduleExpPeriodic {
	from
		se : IDM!ScheduleExpressionPeriodic
	using {
		act : IDM!Activity = IDM!Activity.allInstances()->select(i | i.When.T = se).first();
	}
	to
		tr : PNML!GSPNTimedTransition
		(
			containerPage <- thisModule.getPage,
			id <- act.Name + '_schedule_T',
			Distribution <- se.PeriodDuration
		),
		arc : PNML!GSPNArc
		(
			containerPage <- thisModule.getPage,
			id <- act.Name + '_schedule_T_oarc',
			source <- tr,
			target <- act
		),
		wait : PNML!Place
		(
			containerPage <- thisModule.getPage,
			id <- act.Name + '_schedule_T_wait',
			initialMarking <- thisModule.newPTMarking(1)
		),
		fromwait : PNML!GSPNArc
		(
			containerPage <- thisModule.getPage,
			id <- act.Name + '_schedule_T_fromwait',
			source <- wait,
			target <- tr
		),
		looptowait : PNML!GSPNArc
		(
			containerPage <- thisModule.getPage,
			id <- act.Name + '_schedule_T_looptowait',
			source <- tr,
			target <- wait				
		)
}
	-- EX
rule ScheduleExpTrue {
	from
		se : IDM!ScheduleExpressionTrue
	to
		tt : PNML!OpTrue
}
rule ScheduleExpNot {
	from
		se : IDM!ScheduleExpressionNot
	to
		notexp : PNML!OpNot
		(
			expression <- se.e
		)
}
rule ScheduleExpOr {
	from
		se : IDM!ScheduleExpressionOr
	to
		orexp : PNML!OpOr
		(
			expression1 <- se.e1,
			expression2 <- se.e2
		)
}
rule ScheduleExpAnd {
	from
		se : IDM!ScheduleExpressionAnd
	to
		orexp : PNML!OpAnd
		(
			expression1 <- se.e1,
			expression2 <- se.e2
		)	
}
rule ScheduleExpFailed {
	from 
		se : IDM!ScheduleExpressionFailed
	to
	 	gthan : PNML!OpGreater
		(
			expression1 <- mexp,
			expression2 <- thisModule.newValueExpression(0)
		),
		mexp : PNML!MarkingExpression
		(
			place <- se.failureMode
		)
}
rule ScheduleExpErrorDetected {
	from
		se : IDM!ScheduleExpressionErrorDetected
	to
	 	gthan : PNML!OpGreater
		(
			expression1 <- mexp,
			expression2 <- thisModule.newValueExpression(0)
		),
		mexp : PNML!MarkingExpression
		(
			place <- thisModule.resolveTemp(se.error, 'detected')
		)
}
	-- L
rule ScheduleExpBefore {
	from 
		se : IDM!ScheduleExpressionBefore
	using {
		act : IDM!Activity = IDM!Activity.allInstances()->select(i | i.When.L = se).first();
	}
	to
		limit : PNML!Place
		(
			containerPage <- thisModule.getPage,
			id <- act.Name + '_L',
			initialMarking <- thisModule.newPTMarking(0)
		),
		fireonce : PNML!Place
		(
			containerPage <- thisModule.getPage,
			id <- act.Name + '_L_fireonce',
			initialMarking <- thisModule.newPTMarking(1)
		),	
		elapse : PNML!GSPNTimedTransition
		(
			containerPage <- thisModule.getPage,
			id <- act.Name + '_L_elapse',
			Distribution <- delay
		),
		delay : PNML!Deterministic ( Value <- se.t ),
		from_fireonce : PNML!GSPNArc
		(
			containerPage <- thisModule.getPage,
			id <- fireonce.id + '_to_' + elapse.id,
			source <- fireonce,
			target <- elapse
		),
		to_limit : PNML!GSPNArc
		(
			containerPage <- thisModule.getPage,
			id <- elapse.id + '_to_' + limit.id,
			source <- elapse,
			target <- limit				
		),
		inhibit : PNML!GSPNArc
		(
			containerPage <- thisModule.getPage,
			id <- act.Name + '_L_inhibit',
			source <- limit,
			target <- act.When.T,
			type <- #inhibitor
		)
}
rule ScheduleExpAfter {
	from 
		se : IDM!ScheduleExpressionAfter
	using {
		act : IDM!Activity = IDM!Activity.allInstances()->select(i | i.When.L = se).first();
	}
	to
		limit : PNML!Place
		(
			containerPage <- thisModule.getPage,
			id <- act.Name + '_L',
			initialMarking <- thisModule.newPTMarking(1)
		),
		elapse : PNML!GSPNTimedTransition
		(
			containerPage <- thisModule.getPage,
			id <- act.Name + '_L_elapse',
			Distribution <- delay
		),
		delay : PNML!Deterministic ( Value <- se.t ),
		from_limit : PNML!GSPNArc
		(
			containerPage <- thisModule.getPage,
			id <- limit.id + '_to_' + elapse.id,
			source <- limit,
			target <- elapse				
		),
		inhibit : PNML!GSPNArc
		(
			containerPage <- thisModule.getPage,
			id <- act.Name + '_L_inhibit',
			source <- limit,
			target <- act.When.T,
			type <- #inhibitor
		)
}
rule ScheduleExpInterval {
	from 
		se : IDM!ScheduleExpressionInterval
	using {
		act : IDM!Activity = IDM!Activity.allInstances()->select(i | i.When.L = se).first();
	}
	to
		limit : PNML!Place
		(
			containerPage <- thisModule.getPage,
			id <- act.Name + '_L',
			initialMarking <- thisModule.newPTMarking(1)
		),
		elapse_t1 : PNML!GSPNTimedTransition
		(
			containerPage <- thisModule.getPage,
			id <- act.Name + '_L_elapse_t1',
			Distribution <- delay_t1
		),
		delay_t1 : PNML!Deterministic ( Value <- se.t1 ),
		
		elapse_t2 : PNML!GSPNTimedTransition
		(
			containerPage <- thisModule.getPage,
			id <- act.Name + '_L_elapse_t2',
			Distribution <- delay_t2
		),
		delay_t2 : PNML!Deterministic ( Value <- se.t2 ),
		
		ininterval : PNML!Place
		(
			containerPage <- thisModule.getPage,
			id <- act.Name + '_L_ininterval',
			initialMarking <- thisModule.newPTMarking(0)
		),
		
		from_limit : PNML!GSPNArc
		(
			containerPage <- thisModule.getPage,
			id <- limit.id + '_to_' + elapse_t1.id,
			source <- limit,
			target <- elapse_t1
		),
		enterinterval : PNML!GSPNArc
		(
			containerPage <- thisModule.getPage,
			id <- elapse_t1.id + '_to_' + ininterval.id,
			source <- elapse_t1,
			target <- ininterval
		),
		exitinterval : PNML!GSPNArc
		(
			containerPage <- thisModule.getPage,
			id <- ininterval.id + '_to_' + elapse_t2.id,
			source <- ininterval,
			target <- elapse_t2
		),
		to_limit : PNML!GSPNArc
		(
			containerPage <- thisModule.getPage,
			id <- elapse_t2.id + '_to_' + limit.id,
			source <- elapse_t2,
			target <- limit			
		),
		inhibit : PNML!GSPNArc
		(
			containerPage <- thisModule.getPage,
			id <- act.Name + '_L_inhibit',
			source <- limit,
			target <- act.When.T,
			type <- #inhibitor
		)
}

--Activities
abstract rule Activity {
	from
		act : IDM!Activity
	to
		enabled : PNML!Place
		(
			containerPage <- thisModule.getPage,
			id <- act.Name + '_enabled',
			initialMarking <- thisModule.newPTMarking(0)
		),
		completed : PNML!Place
		(
			containerPage <- thisModule.getPage,
			id <- act.Name + '_completed',
			initialMarking <- thisModule.newPTMarking(0) 	
		),
		tr_success : PNML!GSPNImmediateTransition
		(
			containerPage <- thisModule.getPage,
			id <- act.Name + '_outcome_success',
			Priority <- thisModule.priActivityOutcome
		),
		tr_failed : PNML!GSPNImmediateTransition
		(
			containerPage <- thisModule.getPage,
			id <- act.Name + '_outcome_failed',
			Priority <- thisModule.priActivityOutcome
		),
		tosuccess : PNML!GSPNArc
		(
			containerPage <- thisModule.getPage,
			source <- completed,
			target <- tr_success,
			id <- completed.id + '_to_' + tr_success.id
		),
		tofailed : PNML!GSPNArc
		(
			containerPage <- thisModule.getPage,
			source <- completed,
			target <- tr_failed,
			id <- completed.id + '_to_' + tr_failed.id
		)
}
	--Repair
rule RepairTimed extends Activity {
	from
		act : IDM!RepairActivity
		(
			if act.Duration.oclIsTypeOf(IDM!Deterministic) then
				act.Duration.Value > 0
			else
				true
			endif
		)
	to
		enabled : PNML!Place,
		completed : PNML!Place,
		tr_rep : PNML!GSPNTimedTransition
		(
			containerPage <- thisModule.getPage,
			id <- act.Name,
			Distribution <- act.Duration
		),
		enabledtotr : PNML!GSPNArc
		(
			containerPage <- thisModule.getPage,
			id <- act.Name + '_enabled_to' + enabled.id,
			source <- enabled,
			target <- tr_rep
		),
		trtocompleted : PNML!GSPNArc
		(
			containerPage <- thisModule.getPage,
			source <- tr_rep,
			target <- completed,
			id <- tr_rep.id + '_to_' + completed.id
		),
		tr_success : PNML!GSPNImmediateTransition ( Weight <- act.SuccessProbability ),
		tr_failed : PNML!GSPNImmediateTransition ( Weight <- (1-act.SuccessProbability) )
	do { 
		for( c in act.Target ) {
			thisModule.newOutputArc(tr_success, c);
			thisModule.newInhibitorArc(c, tr_rep);
		}
	}
}
rule RepairImmediate extends Activity {
	from
		act : IDM!RepairActivity
		(
			if act.Duration.oclIsTypeOf(IDM!Deterministic) then
				act.Duration.Value = 0
			else
				false
			endif
		)
	to
		enabled : PNML!Place,
		completed : PNML!Place,
		tr_rep : PNML!GSPNImmediateTransition
		(
			containerPage <- thisModule.getPage,
			id <- act.Name,
			Weight <- 1.0,
			Priority <- thisModule.priActivity
		),
		enabledtotr : PNML!GSPNArc
		(
			containerPage <- thisModule.getPage,
			id <- act.Name + '_enabled_to' + enabled.id,
			source <- enabled,
			target <- tr_rep
		),
		trtocompleted : PNML!GSPNArc
		(
			containerPage <- thisModule.getPage,
			source <- tr_rep,
			target <- completed,
			id <- tr_rep.id + '_to_' + completed.id
		),
		tr_success : PNML!GSPNImmediateTransition ( Weight <- act.SuccessProbability ),
		tr_failed : PNML!GSPNImmediateTransition ( Weight <- (1-act.SuccessProbability) )
	do { 
		for( c in act.Target ) {
			thisModule.newOutputArc(tr_success, c);
			thisModule.newInhibitorArc(c, tr_rep);
		}
	}
}
	--Detection
rule DetectionTimed extends Activity {
	from
		act : IDM!DetectionActivity
		(
			if act.Duration.oclIsTypeOf(IDM!Deterministic) then
				act.Duration.Value > 0
			else
				act.
				true 
			endif
		)
	to
		enabled : PNML!Place,
		completed : PNML!Place,
		tr_rep : PNML!GSPNTimedTransition
		(
			containerPage <- thisModule.getPage,
			id <- act.Name,
			Distribution <- act.Duration
		),
		enabledtotr : PNML!GSPNArc
		(
			containerPage <- thisModule.getPage,
			id <- act.Name + '_enabled_to' + enabled.id,
			source <- enabled,
			target <- tr_rep
		),
		trtocompleted : PNML!GSPNArc
		(
			containerPage <- thisModule.getPage,
			source <- tr_rep,
			target <- completed,
			id <- tr_rep.id + '_to_' + completed.id
		),
		--True Positive (correctly detected)
		tr_success : PNML!GSPNImmediateTransition
		( 
			Weight <- act.Coverage,
			Guard <- g_success				
		),
		g_success : PNML!OpGreater
		(
			expression1 <- thisModule.newMarkingExpression(act.DetectableErrors.first()),
			expression2 <- thisModule.newValueExpression(0)
		),
		tosuccess : PNML!GSPNArc,
		--False Negative (incorrectly not detected)
		tr_failed : PNML!GSPNImmediateTransition
		( 
			Weight <- (1-act.Coverage),
			Guard <- g_failed
		),
		g_failed : PNML!OpGreater
		(
			expression1 <- thisModule.newMarkingExpression(act.DetectableErrors.first()),
			expression2 <- thisModule.newValueExpression(0)
		),
		tofailed : PNML!GSPNArc,
		--True Negative (correctly not detected)
		tr_trueneg : PNML!GSPNImmediateTransition 
		( 
			Weight <- (1-act.FalsePositiveRatio), 
			Guard <- g_trueneg
		),
		g_trueneg : PNML!OpEqual
		(
			expression1 <- thisModule.newMarkingExpression(act.DetectableErrors.first()),
			expression2 <- thisModule.newValueExpression(0)
		),
		totrueneg : PNML!GSPNArc
		(
			containerPage <- thisModule.getPage,
			source <- completed,
			target <- tr_trueneg,
			id <- completed.id + '_to_' + tr_trueneg.id
		),
		--False Positive (incorrectly detected)
		tr_falsepos : PNML!GSPNImmediateTransition
		( 
			Weight <- act.FalsePositiveRatio, 
			Guard <- g_falsepos
		),
		g_falsepos : PNML!OpEqual
		(
			expression1 <- thisModule.newMarkingExpression(act.DetectableErrors.first()),
			expression2 <- thisModule.newValueExpression(0)
		),
		tofalsepos : PNML!GSPNArc
		(
			containerPage <- thisModule.getPage,
			source <- completed,
			target <- tr_falsepos,
			id <- completed.id + '_to_' + tr_falsepos.id
		)
	do { 
		for( c in act.Target ) {
			---thisModule.newOutputArc(tr_success, c);
		}
	}
}


--Evaluation types
rule InstantOfTime {
	from
		idm_instant : IDM!InstantOfTime
	to
		evaltype : PNML!InstantOfTime 
		(
			instant <- thisModule.newVariableExpression(PNML!Variable.allInstances()->select(v | v.name = 'Time').first())
		)
}
rule IntervalOfTime {
	from
		idm_interval : IDM!IntervalOfTime
	to
		evaltype : PNML!IntervalOfTime
		(
			intervalBegin <- thisModule.newValueExpression(idm_interval.begin),
			intervalEnd <- thisModule.newVariableExpression(PNML!Variable.allInstances()->select(v | v.name = 'Time').first())
		)
}
rule IntervalOfTimeAveraged {
	from
		idm_interval : IDM!IntervalOfTimeAveraged
	to
		evaltype : PNML!IntervalOfTimeAveraged
		(
			intervalBegin <- thisModule.newValueExpression(idm_interval.begin),
			intervalEnd <- thisModule.newVariableExpression(PNML!Variable.allInstances()->select(v | v.name = 'Time').first())
		)
}

--Measures of interest
abstract rule MeasureOfInterest {
	from
		idm_measure : IDM!DependabilityMeasure
	to
		measure : PNML!Measure
		(
			name <- idm_measure.Name,
			evaluationType <- idm_measure.evaluations.asSequence().first(),
			rewardFunction <- ite
		),
		ite : PNML!IfThenElse
		(
--			condition <- cond,
			ifTrue <- thisModule.newValueExpression(1),
			ifFalse <- thisModule.newValueExpression(0)
		)
}
rule Reliability extends MeasureOfInterest {
	from 
		idm_measure : IDM!Reliability
	to
		measure : PNML!Measure,
		ite : PNML!IfThenElse
		(
			condition <- cond	
		),
		cond : PNML!OpEqual
		(
			expression1 <- thisModule.newMarkingExpression(relplace),
			expression2 <- thisModule.newValueExpression(0)
		),
		relplace : PNML!Place
		(
			containerPage <- thisModule.getPage,
			id <- measure.name + '_memory_pl',
			initialMarking <- thisModule.newPTMarking(0)
		),
		reltrans : PNML!GSPNImmediateTransition
		(
			containerPage <- thisModule.getPage,
			id <- measure.name + '_memory_tr',
			Weight <- 1.0,
			Priority <- thisModule.priReliability
		),
		relarc : PNML!GSPNArc 
		(
			containerPage <- thisModule.getPage,
			id <- measure.name + '_memory_arc',
			source <- reltrans,
			target <- relplace
		),
		g_and : PNML!OpAnd
		(
--			expression1 <- g_first,
			expression2 <- g_rel
		),
		g_first : PNML!OpGreater
		(
			expression1 <- thisModule.newMarkingExpression(idm_measure.target.first()),
			expression2 <- thisModule.newValueExpression(0)				
		),
		g_rel : PNML!OpEqual
		(
			expression1 <- thisModule.newMarkingExpression(relplace),
			expression2 <- thisModule.newValueExpression(0)
		)
	do {
		thisModule.tmpLogicExp <- g_first;
		for(fm in idm_measure.target.excluding(idm_measure.target.first())) {
			thisModule.tmpLogicExp <- thisModule.newOpOr(
				thisModule.newOpGreater(
					thisModule.newMarkingExpression(fm),
					thisModule.newValueExpression(0)
				),
				thisModule.tmpLogicExp
			);
		}
		g_and.expression1 <- thisModule.tmpLogicExp;
		reltrans.Guard <- g_and;
	}
}
rule Availability extends MeasureOfInterest {
	from 
		idm_measure : IDM!Availability
	to
		measure : PNML!Measure,
		ite : PNML!IfThenElse,
		cond : PNML!OpEqual
		(
			expression1 <- thisModule.newMarkingExpression(idm_measure.target.first()),
			expression2 <- thisModule.newValueExpression(0)
		)
	do {
		thisModule.tmpLogicExp <- cond;
		for(fm in idm_measure.target.subSequence(2, idm_measure.target.size())) {
			thisModule.tmpLogicExp <- thisModule.newOpAnd(
				thisModule.newOpEqual(
					thisModule.newMarkingExpression(fm),
					thisModule.newValueExpression(0)
				),
				thisModule.tmpLogicExp
			);
		}
		ite.condition <- thisModule.tmpLogicExp;
	}
}
rule PFD extends MeasureOfInterest {
	from 
		idm_measure : IDM!FailureProbability
	to
		measure : PNML!Measure,
		ite : PNML!IfThenElse
		(
			condition <- cond	
		),
		cond : PNML!OpGreater
		(
			expression1 <- thisModule.newMarkingExpression(relplace),
			expression2 <- thisModule.newValueExpression(0)
		),
		relplace : PNML!Place
		(
			containerPage <- thisModule.getPage,
			id <- measure.name + '_memory_pl',
			initialMarking <- thisModule.newPTMarking(0)
		),
		reltrans : PNML!GSPNImmediateTransition
		(
			containerPage <- thisModule.getPage,
			id <- measure.name + '_memory_tr',
			Weight <- 1.0,
			Priority <- thisModule.priReliability
		),
		relarc : PNML!GSPNArc 
		(
			containerPage <- thisModule.getPage,
			id <- measure.name + '_memory_arc',
			source <- reltrans,
			target <- relplace
		),
		g_and : PNML!OpAnd
		(
--			expression1 <- g_first,
			expression2 <- g_rel
		),
		g_first : PNML!OpGreater
		(
			expression1 <- thisModule.newMarkingExpression(idm_measure.target.first()),
			expression2 <- thisModule.newValueExpression(0)				
		),
		g_rel : PNML!OpEqual
		(
			expression1 <- thisModule.newMarkingExpression(relplace),
			expression2 <- thisModule.newValueExpression(0)
		)
	do {
		thisModule.tmpLogicExp <- g_first;
		for(fm in idm_measure.target.excluding(idm_measure.target.first())) {
			thisModule.tmpLogicExp <- thisModule.newOpOr(
				thisModule.newOpGreater(
					thisModule.newMarkingExpression(fm),
					thisModule.newValueExpression(0)
				),
				thisModule.tmpLogicExp
			);
		}
		g_and.expression1 <- thisModule.tmpLogicExp;
		reltrans.Guard <- g_and;
	}
}

--Rules to generate expression nodes
lazy rule newVariableExpression {
	from 
		var : PNML!Variable
	to
		vexp : PNML!VariableExpression
		(
			variable <- var
		)
}
lazy rule newValueExpression {
	from
		v : Real
	to
		vexpr : PNML!ValueExpression ( value <- v )
}
rule newMarkingExpression( p : PNML!Place ) {
	to
		m : PNML!MarkingExpression
		(
			place <- p
		)
	do {
		m;
	}
}
rule newOpEqual ( e1 : PNML!ArithmeticExpression, e2 : PNML!ArithmeticExpression) {
	to
		eq : PNML!OpEqual
		(
			expression1 <- e1,
			expression2 <- e2
		)
	do {
		eq;
	}
}
rule newOpGreater ( e1 : PNML!ArithmeticExpression, e2 : PNML!ArithmeticExpression) {
	to
		eq : PNML!OpGreater
		(
			expression1 <- e1,
			expression2 <- e2
		)
	do {
		eq;
	}
}
rule newOpSum ( e1 : PNML!ArithmeticExpression, e2 : PNML!ArithmeticExpression) { 
	to
		sum : PNML!OpSum
		(
			expression1 <- e1,
			expression2 <- e2
		)
	do {
		sum;
	}
}
rule newOpAnd ( e1 : PNML!LogicalExpression, e2 : PNML!LogicalExpression) { 
	to
		opand : PNML!OpAnd
		(
			expression1 <- e1,
			expression2 <- e2
		)
	do { 
		opand;
	}
}
rule newOpOr ( e1 : PNML!LogicalExpression, e2 : PNML!LogicalExpression) { 
	to
		opor : PNML!OpOr
		( 
			expression1 <- e1,
			expression2 <- e2
		)
	do {
		opor;
	}
}
	--Build a LogicalExpression element that represents the fact that the specified
	--component is not failed (i.e., all the corresponding places have marking = 0)
rule buildConditionComponentIsNotFailed(c : IDM!Component) {
	using {
		failures : Sequence(IDM!FailureMode) = c.FailureModes;
		exp : PNML!LogicalExpression = OclUndefined;
	}
	do {
		--Check first failure mode place is > 0
		exp <- thisModule.newOpEqual(
                   thisModule.newMarkingExpression(failures.first()),
				   thisModule.newValueExpression(0)
			   );
		--Check subsequent failure modes (if they exist)
		for(fm in failures.subSequence(2, failures.size())) {
			exp <- thisModule.newOpAnd(
				       exp,
					   thisModule.newOpEqual(
                           thisModule.newMarkingExpression(fm),
				           thisModule.newValueExpression(0)
			           )
				   );
		}
		
		exp;
	}
}
	
	--build a LogicalExpression element that specifies the following condition:
	--The component is not currently affected by any external faults, excluding external faults
	--originated by components that are going to be repaired with the same activity.
	--This prevents repairing a component and having it immediately failed again because of an
	--external fault.
--rule buildConditionNoExternalFaultsExcludingCoRepairs_old(act : IDM!RepairActivity) {
--	using {
--		extfaults : Sequence(IDM!ExternalFault) = act.Target->collect(c | c.Faults).flatten()->select(f | f.oclIsTypeOf(IDM!ExternalFault));
--		extcomponents: Set(IDM!Component) = extfaults->collect(f | f.Source.refImmediateComposite());
--		exp : PNML!LogicalExpression = PNML!OpTrue.newInstance();
--	}
--	do {
--		for(xft in extfaults) {
--			if(not act.Target.includes(xft.Source.Component)) {
--				exp <- thisModule.newOpAnd(
--						   exp,
--					       thisModule.newOpEqual(
--					           thisModule.newMarkingExpression(xft.Source),
--							   thisModule.newValueExpression(0)
--						   )
--					   );
--			}
--		}
--		--enable the transition if at least one of the components is going to be repaired
--		for(c in extcomponents) {
--			exp <- thisModule.newOpOr(
--				       exp,
--				       thisModule.newOpGreater(
--				           thisModule.newMarkingExpression(c),
--						   thisModule.newValueExpression(0)
--					   )
--				   );
--		}
--		exp;
--	}
--}
rule buildConditionNoExternalFaultsExcludingCoRepairs(c : IDM!Component) {
	using {
		extfaults : Sequence(IDM!ExternalFault) = c.Faults->select(f | f.oclIsTypeOf(IDM!ExternalFault));
		extcomponents: Set(IDM!Component) = extfaults->collect(f | f.Source.refImmediateComposite());
		exp : PNML!LogicalExpression = PNML!OpTrue.newInstance();
		expout: PNML!LogicalExpression = PNML!OpTrue.newInstance();
	}
	do {
		--For all components that propagate to this component...
		for(xc in extcomponents) {
			exp <- PNML!OpTrue.newInstance();
			--for all external faults, check that they are not active
			for(xft in extfaults->select(f | f.Source.refImmediateComposite() = xc)) {
				exp <- thisModule.newOpAnd(
						   exp,
					       thisModule.newOpEqual(
					           thisModule.newMarkingExpression(xft.Source),
							   thisModule.newValueExpression(0)
						   )
					   );
			}
			--or that the component is going to be repaired
			exp <- thisModule.newOpOr(
				       exp,
					   thisModule.newOpGreater(
					       thisModule.newMarkingExpression(xc),
						   thisModule.newValueExpression(0)
					   )
				   );
			expout <- thisModule.newOpAnd(expout, exp);
		}
		expout;
	}
}
	
--Other rules
	--Creates a new output arc between a transition and a place
rule newOutputArc ( t : PNML!Transition, p : PNML!Place ) { 
	to
		arc : PNML!GSPNArc
		(
			containerPage <- thisModule.getPage,
			source <- t,
			target <- p,
			id <- t.toString() + '_to_' + p.toString()
		)
}
	--Creates a new input arc between a place and a transition
rule newInputArc ( p : PNML!Place, t : PNML!Transition ) {
	to 
		arc : PNML!GSPNArc
		(
			containerPage <- thisModule.getPage,
			source <- p,
			target <- t,
			id <- p.toString() + '_to_' + t.toString()
		)
}
	--Creates a new inhibitor arc between a place and a transition
rule newInhibitorArc ( p : PNML!Place, t : PNML!Transition ) {
	to 
		arc : PNML!GSPNArc
		(
			containerPage <- thisModule.getPage,
			source <- p,
			target <- t,
			id <- p.toString() + '_inhibits_' + t.toString(),
			type <- #inhibitor
		)
}
	--Creates a new input arc between a place and a transition,
	--having as multiplicity the number of tokens in the place (i.e., MARK(p))
rule newInputArcMultiplicityOfPlace ( p : PNML!Place, t : PNML!Transition ) {
	to 
		arc : PNML!GSPNArc
		(
			containerPage <- thisModule.getPage,
			source <- p,
			target <- t,
			id <- p.toString() + '_to_' + t.toString(),
			MultiplicityFunction <- expmark
		),
	    expmark : PNML!MarkingExpression
		(
			place <- p	
		)
}
	--Creates a new "PTMarking" element from on an integer value
lazy rule newPTMarking {
	from
		v : Integer
	to
		m : PNML!PTMarking (
			text <- v
		)
}
	
---FINAL RULE---
--One of the purposes of this rule is to ensure that all the InternalPropagation
--transitions that have the same 'Source' errors are mutually exclusive.
--This is a workaround to avoid strange behavior in the petroleum use case
endpoint rule Finalize() {
	using {
		errSet : Set(IDM!Error) = Set{};
		errSetMap : Map(Set(IDM!Error),PNML!Place) = Map{};
		tmpPlace : PNML!Place = OclUndefined;
		j : Integer = 0;
	}
	do {		
		--Loop through all the InternalPropagation elements, and find those
		--that have the same set of Error elements as their Source attribute
		--Create a place for each set, and store a reference in a map
		for(ip in IDM!InternalPropagation.allInstances()) {
			errSet <- ip.Source;

			if(errSetMap->get(errSet).oclIsUndefined()) {
				j <- j+1;				
				tmpPlace <- PNML!Place.newInstance();
				
				tmpPlace.containerPage <- PNML!Page.allInstances()->first();
				tmpPlace.id <- 'stopper' + j;
				tmpPlace.initialMarking <- thisModule.newPTMarking(1);
				
				errSetMap <- errSetMap.including(errSet, tmpPlace);
			}
		}
		
		--Loop again through all the InternalPropagation elements,
		--this time we add a transition between the place previously created
		--and the transition that represents the InternalPropagation element
		for(ip in IDM!InternalPropagation.allInstances()) {
			errSet <- ip.Source;
			tmpPlace <- errSetMap->get(errSet);
			
			thisModule.newInputArc(
				tmpPlace, 
				thisModule.resolveTemp(ip, 'triprop')
			);
		}	
	}
}