muMLE/examples/semantics/translational/merged_mm.od

# Auto-generated by /home/maestro/repos/MV2/examples/semantics/translational/regenerate_mm.py.

# Merged run-time meta-models of 'Petri Net' and 'Port' formalisms.
# An abstract 'Top'-class (superclass of everything else), and a 'generic_link'-association (which can connect everything with everything) have also been added.

# PlantUML visualization: https://deemz.org/plantuml/pdf/hPTFYzim4CNl_XGYnqA27P8uDgM7tSEobsmWWHw3RCk9Y2CPMIcKThzxHyuViiMGPwCSzhJpqxoPfz4uo2lUD6pqockUI_lxLQl66YwLPIF66nPUVxkEF-ut2uk8_GaOQmwola5OojwL5NjXWi_WUi1wjQvuBZQMMm6ZborQdKzRVHIgwUB-rEOep4RW-POtw2MqazehJR4WucV0CrUvtB97HdckO4pHZT5dawEvH25l8RUkLZe_icWoYS3mQTmMnygJw2hBYp3sqASsqPnVt44nPrVfZJLIxJjaRdMDCkFuKMDhApGqcJs6thtJIrAIFJBQag2XVFeO-YQKCDng0uSdNuIljeQhHbgf5Kh8mawFhLTqxvN8BSygk0vPtErNgOueelZIZciE9ATNFyhB03hfNtI3KlQYTIMu-iyW_OZtkREXgTOv8AxZ32QMhT3WwN-wAV3zxtZyd3ahn7ESkoiOZkQuJnorrYTkFaDmTBl1xFZKPoleJG6oez4CPfS0Ojsh0-BAfLUZY8LNeuJSAsuQ-nLR-3GArDaUOZD0R0-Z91cGNG5VCaWipLeGDqUCak6r2_rUCg_ZarPVhnE59rvjZ8pF7gqeI-XbNB1Hn2OJHiliUFo3djuHjbMdJ2FpcV9ro1OTkdE-0NmNbJ9kSa00VNdS3uZW0sXdJ5dErKVjbaNapI_BGK92EaUgmmuIuxmtu10Q7YJclkSXHLiEwBehGSfgjOCQ7mzgVEmQltShlCnt5Iszo8AI3JcfTO1iBWPmNqz0rQ8XLalQxbm_uZ_AVm==


CapacityConstraint:Class
PNPlaceState:Class
WorkerSet:Class
State:Class
Stateful:Class {
    abstract = True;
}
Source:Class {
    abstract = True;
}
Clock:Class {
    lower_cardinality = 1;
    upper_cardinality = 1;
}
BerthState:Class {
    constraint = ```
        errors = []
        numShips = get_slot_value(this, "numShips")
        status = get_slot_value(this, "status")
        if (numShips == 0) != (status == "empty"):
            errors.append(f"Inconsistent: numShips = {numShips}, but status = {status}")
        errors
    ```;
}
Top:Class {
    abstract = True;
}
Place:Class
WorkerSetState:Class
Berth:Class
Generator:Class
PNTransition:Class
PNConnectable:Class {
    abstract = True;
}
Sink:Class {
    abstract = True;
}
ConnectionState:Class
PlaceState:Class
PNPlace:Class
shipCapacities:GlobalConstraint {
    constraint = ```
        errors = []
        for _, constr in get_all_instances("CapacityConstraint"):
            cap = get_slot_value(constr, "shipCapacity")
            total = 0
            place_names = [] # for debugging
            for lnk in get_outgoing(constr, "capacityOf"):
                place = get_target(lnk)
                place_names.append(get_name(place))
                place_state = get_source(get_incoming(place, "of")[0])
                total += get_slot_value(place_state, "numShips")
            if total > cap:
                errors.append(f"The number of ships in places {','.join(place_names)} ({total}) exceeds the capacity ({cap}) of CapacityConstraint {get_name(constr)}.")
        errors
    ```;
}
operatingCapacities:GlobalConstraint {
    constraint = ```
        errors = []
        for _, workersetstate in get_all_instances("WorkerSetState"):
            workerset = get_target(get_outgoing(workersetstate, "of")[0])
            num_operating = len(get_outgoing(workersetstate, "isOperating"))
            num_workers = get_slot_value(workerset, "numWorkers")
            if num_operating > num_workers:
                errors.append(f"WorkerSet {get_name(workerset)} is operating more berths ({num_operating}) than there are workers ({num_workers})")
        errors
    ```;
}
WorkerSet_numWorkers:AttributeLink (WorkerSet -> Integer) {
    name = "numWorkers";
    constraint = `get_value(get_target(this)) >= 0`;
    optional = False;
}
PlaceState_numShips:AttributeLink (PlaceState -> Integer) {
    constraint = `get_value(get_target(this)) >= 0`;
    optional = False;
    name = "numShips";
}
ConnectionState_moved:AttributeLink (ConnectionState -> Boolean) {
    name = "moved";
    constraint = ```
        result = True
        all_successors_moved = True
        moved = get_value(get_target(this))
        conn_state = get_source(this)
        conn = get_target(get_outgoing(conn_state, "of")[0])
        tgt_place = get_target(conn)
        next_conns = get_outgoing(tgt_place, "connection")
        for next_conn in next_conns:
            next_conn_state = get_source(get_incoming(next_conn, "of")[0])
            if not get_slot_value(next_conn_state, "moved"):
                all_successors_moved = False
        if moved and not all_successors_moved:
            result = f"Connection {get_name(conn)} played before its turn."
        result
    ```;
    optional = False;
}
BerthState_status:AttributeLink (BerthState -> String) {
    optional = False;
    name = "status";
    constraint = ```
        (
                    get_value(get_target(this)) in { "empty", "unserved", "served" }
                )
    ```;
}
PNPlaceState_numTokens:AttributeLink (PNPlaceState -> Integer) {
    name = "numTokens";
    constraint = `"numTokens cannot be negative" if get_value(get_target(this)) < 0 else None`;
    optional = False;
}
Clock_time:AttributeLink (Clock -> Integer) {
    optional = False;
    name = "time";
    constraint = `get_value(get_target(this)) >= 0`;
}
CapacityConstraint_shipCapacity:AttributeLink (CapacityConstraint -> Integer) {
    optional = False;
    name = "shipCapacity";
    constraint = `get_value(get_target(this)) >= 0`;
}
of:Association (State -> Stateful) {
    target_lower_cardinality = 1;
    source_upper_cardinality = 1;
    source_lower_cardinality = 1;
    target_upper_cardinality = 1;
}
arc:Association (PNConnectable -> PNConnectable)
canOperate:Association (WorkerSet -> Berth) {
    target_lower_cardinality = 1;
}
inh_arc:Association (PNPlace -> PNTransition)
connection:Association (Source -> Sink)
pn_of:Association (PNPlaceState -> PNPlace) {
    source_upper_cardinality = 1;
    source_lower_cardinality = 1;
    target_upper_cardinality = 1;
    target_lower_cardinality = 1;
}
generic_link:Association (Top -> Top)
isOperating:Association (WorkerSetState -> Berth) {
    constraint = ```
        errors = []
        
        # get status of Berth
        berth = get_target(this)
        berth_state = get_source(get_incoming(berth, "of")[0])
        status = get_slot_value(berth_state, "status")
        if status != "unserved":
            errors.append(f"Cannot operate {get_name(berth)} because there is no unserved ship there.")
        
        # only operate Berts that we can operate
        workerset = get_target(get_outgoing(get_source(this), "of")[0])
        can_operate = [get_target(lnk) for lnk in get_outgoing(workerset, "canOperate")]
        if berth not in can_operate:
            errors.append(f"Cannot operate {get_name(berth)}.")
        
        errors
    ```;
}
capacityOf:Association (CapacityConstraint -> Place) {
    target_lower_cardinality = 1;
}
:Inheritance (connection -> Stateful)
:Inheritance (CapacityConstraint -> Top)
:Inheritance (Sink -> Top)
:Inheritance (generic_link -> Top)
:Inheritance (Berth -> Place)
:Inheritance (WorkerSet -> Stateful)
:Inheritance (Place -> Source)
:Inheritance (PlaceState -> State)
:Inheritance (State -> Top)
:Inheritance (Source -> Top)
:Inheritance (Clock -> Top)
:Inheritance (Stateful -> Top)
:Inheritance (Place -> Stateful)
:Inheritance (PNConnectable -> Top)
:Inheritance (WorkerSetState -> State)
:Inheritance (Place -> Sink)
:Inheritance (BerthState -> PlaceState)
:Inheritance (PNTransition -> PNConnectable)
:Inheritance (ConnectionState -> State)
:Inheritance (PNPlaceState -> Top)
:Inheritance (Generator -> Source)
:Inheritance (Berth -> Stateful)
:Inheritance (PNPlace -> PNConnectable)