import models/RAM_PetriNets_Runtime_Runtime as RAM_PN_R
include "primitives.alh"
include "modelling.alh"

RAM_PN_R s {
    Composite schedule {
        {Contains} Failure failure {}
        {Contains} Success success {}
        {Contains} Atomic mark {
            LHS {
                Pre_PetriNets_Runtime/Transition {
                    label = "1"
                }
            }
            NAC {
				Pre_PetriNets_Runtime/Transition mark_nac_t {
					label = "1"
				}
				Pre_PetriNets_Runtime/Place mark_nac_p{
					label = "10"
				}
				Pre_PetriNets_Runtime/P2T (mark_nac_p, mark_nac_t){
					label = "11"
				}
				constraint = $
					Boolean function constraint(host_model : Element, mapping : Element):
						Integer tokens
						Integer weight
						tokens = read_attribute(host_model, mapping["10"], "tokens")
						weight = read_attribute(host_model, mapping["11"], "weight")
                        return (tokens < weight)!
					$
            }
            RHS {
                Post_PetriNets_Runtime/Transition {
                    label = "1"
                    value_executing = $
                        Boolean function value(host_model : Element, name : String, mapping : Element):
                            return True!
                        $
                }
            }
        }
        {Contains} ForAll consume {
            LHS {
                Pre_PetriNets_Runtime/Transition lhs_consume_t{
                    label = "0"
                    constraint_executing = $
                        Boolean function constraint(value : Boolean):
                            return value!
                        $
                }
                Pre_PetriNets_Runtime/Place lhs_consume_p{
                    label = "1"
                }
                Pre_PetriNets_Runtime/P2T lhs_consume_p2t(lhs_consume_p, lhs_consume_t){
                    label = "2"
                }
            }
            RHS {
                Post_PetriNets_Runtime/Transition rhs_consume_t {
                    label = "0"
                }
                Post_PetriNets_Runtime/Place rhs_consume_p {
                    label = "1"
                    value_tokens = $
                        Integer function value(host_model : Element, name : String, mapping : Element):
                            return integer_subtraction(read_attribute(host_model, name, "tokens"), read_attribute(host_model, mapping["2"], "weight"))!
                        $
                }
                Post_PetriNets_Runtime/P2T (rhs_consume_p, rhs_consume_t){
                    label = "2"
                }
            }
        }
        {Contains} ForAll produce {
            LHS {
                Pre_PetriNets_Runtime/Transition lhs_produce_t{
                    label = "0"
                    constraint_executing = $
                        Boolean function constraint(value : Boolean):
                            return value!
                        $
                }
                Pre_PetriNets_Runtime/Place lhs_produce_p{
                    label = "1"
                }
                Pre_PetriNets_Runtime/T2P (lhs_produce_t, lhs_produce_p){
                    label = "2"
                }
            }
            RHS {
                Post_PetriNets_Runtime/Transition rhs_produce_t{
                    label = "0"
                }
                Post_PetriNets_Runtime/Place rhs_produce_p{
                    label = "1"
                    value_tokens = $
                        Integer function value(host_model : Element, name : String, mapping : Element):
                            return integer_addition(read_attribute(host_model, name, "tokens"), read_attribute(host_model, mapping["2"], "weight"))!
                        $
                }
                Post_PetriNets_Runtime/T2P (rhs_produce_t, rhs_produce_p){
                    label = "2"
                }
            }
        }
        {Contains} Atomic unmark_transition {
            LHS {
                Pre_PetriNets_Runtime/Transition {
                    label = "0"
                    constraint_executing = $
                        Boolean function constraint(value : Boolean):
                            return value!
                        $
                }
            }
            RHS {
                Post_PetriNets_Runtime/Transition {
                    label = "0"
                    value_executing = $
                        Boolean function value(host_model : Element, name : String, mapping : Element):
                            return False!
                        $
                }
            }
        }
    }
    OnSuccess (mark, consume) {}
    OnFailure (mark, failure) {}
    OnSuccess (consume, produce) {}
    OnFailure (consume, produce) {}
    OnSuccess (produce, unmark_transition) {}
    OnFailure (produce, unmark_transition) {}
    OnSuccess (unmark_transition, success) {}
    OnFailure (unmark_transition, failure) {}
    Initial (schedule, mark) {}
}

export s to models/pn_simulate