modelverse/integration/code/pn_simulate.mvc

include "primitives.alh"
include "modelling.alh"

Composite schedule {
    {Contains} Failure failure {}
    {Contains} Success success {}
    {Contains} Atomic mark {
        LHS {
            Pre_PetriNet_Runtime/Transition {
                label = "1"
            }
        }
        NAC {
    			Pre_PetriNet_Runtime/Transition mark_nac_t {
    				label = "1"
    			}
    			Pre_PetriNet_Runtime/Place mark_nac_p{
    				label = "10"
    			}
    			Pre_PetriNet_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_PetriNet_Runtime/Transition {
                label = "1"
                value_executing = $
                    Boolean function value(host_model : Element, name : String, mapping : Element):
                        return True!
                    $
            }
        }
    }
    {Contains} ForAll consume {
        LHS {
            Pre_PetriNet_Runtime/Transition lhs_consume_t{
                label = "0"
                constraint_executing = $
                    Boolean function constraint(value : Boolean):
                        return value!
                    $
            }
            Pre_PetriNet_Runtime/Place lhs_consume_p{
                label = "1"
            }
            Pre_PetriNet_Runtime/P2T lhs_consume_p2t(lhs_consume_p, lhs_consume_t){
                label = "2"
            }
        }
        RHS {
            Post_PetriNet_Runtime/Transition rhs_consume_t {
                label = "0"
            }
            Post_PetriNet_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_PetriNet_Runtime/P2T (rhs_consume_p, rhs_consume_t){
                label = "2"
            }
        }
    }
    {Contains} ForAll produce {
        LHS {
            Pre_PetriNet_Runtime/Transition lhs_produce_t{
                label = "0"
                constraint_executing = $
                    Boolean function constraint(value : Boolean):
                        return value!
                    $
            }
            Pre_PetriNet_Runtime/Place lhs_produce_p{
                label = "1"
            }
            Pre_PetriNet_Runtime/T2P (lhs_produce_t, lhs_produce_p){
                label = "2"
            }
        }
        RHS {
            Post_PetriNet_Runtime/Transition rhs_produce_t{
                label = "0"
            }
            Post_PetriNet_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_PetriNet_Runtime/T2P (rhs_produce_t, rhs_produce_p){
                label = "2"
            }
        }
    }
    {Contains} Atomic unmark_transition {
        LHS {
            Pre_PetriNet_Runtime/Transition {
                label = "0"
                constraint_executing = $
                    Boolean function constraint(value : Boolean):
                        return value!
                    $
            }
        }
        RHS {
            Post_PetriNet_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) {}