import models/SimpleClassDiagrams as SCD
include "primitives.alh"

SCD PetriNets{
    Class Natural {
        $
            if (bool_not(is_physical_int(self))):
                return "Natural has no integer value at " + name!
            elif (integer_lt(self, 0)):
                return "Natural does not have a positive or zero value at " + name!
            else:
                return "OK"!
         $
    }
    Class Place{
        tokens : Natural {
            target_lower_cardinality = 1
            target_upper_cardinality = 1
            }
    }
    Class Transition{}
    Association P2T (Place, Transition) {
        weight : Natural {
            target_lower_cardinality = 1
            target_upper_cardinality = 1
            }
    }
    Association T2P (Transition, Place) {
        weight : Natural {
            target_lower_cardinality = 1
            target_upper_cardinality = 1
            }
    }
}

PetriNets valid_petrinet {
    Place p1 {
        tokens = 1
    }
    Place p2 {
        tokens = 3
    }
    Transition t1 {}
    P2T (p1, t1) {
        weight = 1
    }
    T2P (t1, p2) {
        weight = 2
    }
}

PetriNets invalid_petrinet_1 {
    Place p1 {
        tokens = -1
    }
    Place p2 {
        tokens = 3
    }
    Transition t1 {}
    P2T (p1, t1) {
        weight = 1
    }
    T2P (t1, p2) {
        weight = 2
    }
}

PetriNets invalid_petrinet_2 {
    Place p1 {
        tokens = 1
    }
    Place p2 {
        tokens = 3
    }
    Transition t1 {}
    P2T p2t(p1, t1) {
        weight = -1
    }
    T2P (t1, p2) {
        weight = 2
    }
}

PetriNets invalid_petrinet_3 {
    Place p1 {
        tokens = 1
    }
    Place p2 {
        tokens = 3
    }
    Transition t1 {}
    P2T wrong_p2t (p1, p2) {
        weight = 1
    }
    T2P (t1, p2) {
        weight = 2
    }
}

PetriNets invalid_petrinet_4 {
    Place p1 {
        tokens = 1
    }
    Place p2 {
        tokens = 3
    }
    Transition t1 {}
    P2T (p1, t1) {
        weight = 1
    }
    T2P wrong_t2p(p1, p2) {
        weight = 2
    }
}

PetriNets invalid_petrinet_5 {
    Place p1 {}
    Place p2 {
        tokens = 3
    }
    Transition t1 {}
    P2T (p1, t1) {
        weight = 1
    }
    T2P (t1, p2) {
        weight = 2
    }
}

PetriNets invalid_petrinet_6 {
    Place p1 {
        tokens = 1
    }
    Place p2 {
        tokens = 3
    }
    Transition t1 {}
    P2T p2t (p1, t1) {}
    T2P (t1, p2) {
        weight = 2
    }
}

PetriNets invalid_petrinet_7 {
    Place p1 {
        tokens = "abc"
    }
    Place p2 {
        tokens = 3
    }
    Transition t1 {}
    P2T (p1, t1) {
        weight = 1
    }
    T2P (t1, p2) {
        weight = 2
    }
}

export PetriNets to models/PetriNets
export valid_petrinet to models/valid_petrinet
export invalid_petrinet_1 to models/invalid_petrinet_1
export invalid_petrinet_2 to models/invalid_petrinet_2
export invalid_petrinet_3 to models/invalid_petrinet_3
export invalid_petrinet_4 to models/invalid_petrinet_4
export invalid_petrinet_5 to models/invalid_petrinet_5
export invalid_petrinet_6 to models/invalid_petrinet_6
export invalid_petrinet_7 to models/invalid_petrinet_7