import * as _ from 'lodash';
import { PetriNet, Transition, InFlow, OutFlow, TransitionObject, InFlowObject, OutFlowObject, TransitionExtensions, TokenObject, PetriNetObject, PlaceObject } from './coloredPetriNets';
import { NameSuggester, crossProduct } from './utils';
import { GlobalReadTransitionPlusPlus, GlobalWriteTransitionPlusPlus, GlobalUpdateTransitionPlusPlus, TransitionPlusPlus, PrintLnTransitionPlusPlus, CallTransitionPlusPlus, ReturnTransitionPlusPlus, StartAgentTransitionPlusPlus, JoinTransitionPlusPlus, InitChanTransitionPlusPlus, SendTransitionPlusPlus, ReceiveTransitionPlusPlus, DefaultTransitionPlusPlus, MutexInitTransitionPlusPlus, MutexLockTransitionPlusPlus, MutexUnlockTransitionPlusPlus, ConditionInitTransitionPlusPlus, ConditionAwaitTransitionPlusPlus, ConditionSignalTransitionPlusPlus } from './coloredPetriNetsPlusPlus';

import { runtimeTags, extraTagsOf, mergeExtraTags } from './tagging';

const getFreeIdentifierForPattern = function (preferredName: string, pattern: string): string { // return an identifier that is guaranteed not to occur in a pattern
    if (!pattern.includes(preferredName)) {
        return preferredName;
    } else {
        // naming conflict
        // dumb resolution strategy: append something random
        return getFreeIdentifierForPattern(preferredName + Math.random().toString(36).substring(2, 3), pattern);
    }
};


const compile = function (input: PetriNet): PetriNet {
    "use strict";

    const placeNameSuggester = new NameSuggester();
    const transitionNameSuggester = new NameSuggester();

    // compile normal places

    const outPlaces: PlaceObject[] = _.map(input.places, (inPlace) => {
        const newKey = placeNameSuggester.suggestName(inPlace.key);
        return {
            key: newKey,
            displayName: inPlace.displayName,
            extensions: inPlace.extensions
        };
    });

    // add helper places

    const agentGeneratorPlaceKey = placeNameSuggester.suggestName("agent-generator");
    outPlaces.push({
        key: agentGeneratorPlaceKey,
        displayName: "agent generator",
        extensions: {
            extraTag: runtimeTags.lifecycle
        }
    });

    const agentGraveyardPlaceKey = placeNameSuggester.suggestName("agent-graveyard");
    outPlaces.push({
        key: agentGraveyardPlaceKey,
        displayName: "agent graveyard",
        extensions: {
            extraTag: runtimeTags.lifecycle
        }
    });

    const mutexGeneratorPlaceKey = placeNameSuggester.suggestName("mutex-gen");
    outPlaces.push({
        key: mutexGeneratorPlaceKey,
        displayName: "mutex generator",
        extensions: {
            extraTag: runtimeTags.mutexes
        }
    });

    const mutexStorePlaceKey = placeNameSuggester.suggestName("mutex-store");
    outPlaces.push({
        key: mutexStorePlaceKey,
        displayName: "mutex store",
        extensions: {
            extraTag: runtimeTags.mutexes
        }
    });

    const asyncChanGenPlaceKey = placeNameSuggester.suggestName("async-chan-gen");
    outPlaces.push({
        key: asyncChanGenPlaceKey,
        displayName: "asynchronous channel generator",
        extensions: {
            extraTag: runtimeTags.messagePassing
        }
    });

    const syncChanGenPlaceKey = placeNameSuggester.suggestName("sync-chan-gen");
    outPlaces.push({
        key: syncChanGenPlaceKey,
        displayName: "synchronous channel generator",
        extensions: {
            extraTag: runtimeTags.messagePassing
        }
    });

    const asyncChanStorePlaceKey = placeNameSuggester.suggestName("async-chan-store");
    outPlaces.push({
        key: asyncChanStorePlaceKey,
        displayName: "asynchronous channel store",
        extensions: {
            extraTag: runtimeTags.messagePassing
        }
    });

    const conditionGeneratorPlaceKey = placeNameSuggester.suggestName("condition-gen");
    outPlaces.push({
        key: conditionGeneratorPlaceKey,
        displayName: "condition generator",
        extensions: {
            extraTag: runtimeTags.conditions.parent,
        }
    });

    const conditionStorePlaceKey = placeNameSuggester.suggestName("condition-store");
    outPlaces.push({
        key: conditionStorePlaceKey,
        displayName: "condition store",
        extensions: {
            extraTag: runtimeTags.conditions.row
        }
    });

    const conditionSignalRelayReadyPlaceKey = placeNameSuggester.suggestName("condition-signal-relay-ready");
    outPlaces.push({
        key: conditionSignalRelayReadyPlaceKey,
        displayName: "condition signal relay system (ready)",
        extensions: {
            extraTag: runtimeTags.conditions.parent
        }
    });

    const conditionSignalRelaySignalingPlaceKey = placeNameSuggester.suggestName("condition-signal-relay-signaling");
    outPlaces.push({
        key: conditionSignalRelaySignalingPlaceKey,
        displayName: "condition signal relay system (signaling)",
        extensions: {
            extraTag: runtimeTags.conditions.row
        }
    });


    // add global variable store places

    const globalVariablePlaceKeys: { [variable: string]: string } = {};
    _.each(input.transitions, (transition) => {
        if (transition instanceof GlobalReadTransitionPlusPlus || transition instanceof GlobalWriteTransitionPlusPlus || transition instanceof GlobalUpdateTransitionPlusPlus) {
            if (!_.has(globalVariablePlaceKeys, transition.variable)) {
                const variablePlaceKey = placeNameSuggester.suggestName("global-" + transition.variable);

                globalVariablePlaceKeys[transition.variable] = variablePlaceKey;

                outPlaces.push({
                    key: variablePlaceKey,
                    displayName: "global-" + transition.variable,
                    extensions: {
                        extraTag: runtimeTags.globalVars,
                        plusplus: {
                            type: 'global-variable',
                            variableName: transition.variable
                        }
                    }
                });
            }
        }
    });


    const outTransitions: TransitionObject[] = [];


    // add fixed transitions for signaling system

    outTransitions.push({
        key: transitionNameSuggester.suggestName('condition-signal-relay-return'),
        displayName: "return condition signal relay to state ready",
        guard: `agents == 0`,
        inFlows: [
            {
                source: conditionSignalRelaySignalingPlaceKey,
                pattern: `{ condition }`
            },
            {
                source: conditionStorePlaceKey,
                pattern: `{ mutex, condition, agents }`
            }
        ],
        outFlows: [
            {
                target: conditionSignalRelayReadyPlaceKey,
                expression: `{}`
            },
            {
                target: conditionStorePlaceKey,
                expression: `{ mutex, condition, agents }`
            }
        ],
        extensions: {
            extraTag: runtimeTags.conditions.parent
        }
    });


    // compile transitions

    const extractUniqueInOutFlows = function (inTransition: Transition): { inFlow: InFlow; outFlow: OutFlow } {
        if (inTransition.inFlows.length !== 1 || inTransition.outFlows.length !== 1)
            throw new Error(`The transition ${inTransition.key} (${inTransition.displayName}) was expected to have exactly one incoming and one outgoing flow.`);

        return {
            inFlow: inTransition.inFlows[0],
            outFlow: inTransition.outFlows[0]
        };
    };

    const compileGeneralPurposeTransition = function (inTransition: Transition): void {
        const { inFlow, outFlow } = extractUniqueInOutFlows(inTransition);

        if (inFlow.pattern == null) throw new Error("Missing pattern on general-purpose transition.");
        const freeAgentIdentifier = getFreeIdentifierForPattern('agent', inFlow.pattern);

        outTransitions.push({
            key: transitionNameSuggester.suggestName(inTransition.key),
            displayName: inTransition.displayName,
            guard: `${inTransition.guard}`,
            inFlows: [{
                source: inFlow.source.key,
                pattern: `{ ${freeAgentIdentifier}, vars: ${inFlow.pattern} }`
            }],
            outFlows: [{
                target: outFlow.target.key,
                expression: `{ ${freeAgentIdentifier}, vars: (${outFlow.expression}) }`
            }],
            extensions: {
                extraTag: extraTagsOf(inTransition),
            }
        });
    };

    const addDefaultGuardPatternExpression = function ({ key, displayName, inFlows, outFlows, extensions }: { key: string; displayName: string; inFlows: InFlowObject[]; outFlows: OutFlowObject[]; extensions: TransitionExtensions }): TransitionObject {
        return {
            key,
            displayName,
            guard: 'true',
            inFlows: _.map(inFlows, ({ source }) => ({ source, pattern: '{ agent, vars }' })),
            outFlows: _.map(outFlows, ({ target }) => ({ target, expression: '{ agent, vars }' })),
            extensions
        };
    };

    const compilePrintLnTransitionPlusPlus = function (inTransition: PrintLnTransitionPlusPlus): void {
        if (inTransition.inFlows.length !== 1 || inTransition.outFlows.length !== 1) throw new Error("println transitions must have one inflow and one outflow");
        outTransitions.push(addDefaultGuardPatternExpression({
            key: transitionNameSuggester.suggestName(inTransition.key),
            displayName: inTransition.displayName,
            inFlows: inTransition.inFlowsAsObject(),
            outFlows: inTransition.outFlowsAsObject(),
            extensions: {
                extraTag: extraTagsOf(inTransition),
                println: `eval(${inTransition.expression}, vars)`
            }
        }));
    };

    const callLinkHooks: {
        awaitingReturnPlaceKey: string;
        nextPlaceKey: string;
        returnVariable: string;
        extraTag: string;
    }[] = [];

    const compileCallTransitionPlusPlus = function (inTransition: CallTransitionPlusPlus): void {
        if (inTransition.inFlows.length !== 1 || inTransition.outFlows.length !== 2) throw new Error("call transitions must have one inflow and two outflows");

        const callingPlace = inTransition.inFlows[0].source;
        const calleeStartPlace = inTransition.outFlows[1].target;

        const awaitingReturnPlaceKey = placeNameSuggester.suggestName(inTransition.key + "-awaiting-return");

        callLinkHooks.push({
            extraTag: mergeExtraTags(inTransition, ["awaiting-return", "awaiting-place"]),
            awaitingReturnPlaceKey,
            nextPlaceKey: inTransition.outFlows[0].target.key,
            returnVariable: inTransition.return
        });

        outPlaces.push({
            key: awaitingReturnPlaceKey,
            displayName: "awaiting return",
            extensions: {
                extraTag: mergeExtraTags(inTransition, ["awaiting-return", "awaiting-place"]),
                sourcemap: callingPlace.extensions.sourcemap
            }
        });

        let argsExpression = "";
        _.each(inTransition.arguments, (argument) => {
            if (argsExpression) argsExpression += ', ';
            argsExpression += argument.name + ' : eval(' + argument.expression + ', vars)';
        });

        outTransitions.push({
            key: transitionNameSuggester.suggestName(inTransition.key),
            displayName: inTransition.displayName,
            guard: 'true',
            inFlows: [
                {
                    source: inTransition.inFlows[0].source.key,
                    pattern: '{ agent, vars }'
                }
            ],
            outFlows: [
                {
                    target: awaitingReturnPlaceKey,
                    expression: '{ agent, vars }'
                },
                {
                    target: calleeStartPlace.key,
                    expression: `{ agent: { id : agent.id, rd : agent.rd + 1 }, vars : { ${argsExpression} } }`
                }
            ],
            extensions: {
                extraTag: extraTagsOf(inTransition),
                plusplus: {
                    type: "call"
                }
            }
        });
    };

    const returnLinkHooks: { returningPlaceKey: string }[] = [];

    type HandshakeLinkHook = {
        offeringPlaceKey: string;
        syncCompletedPlaceKey: string;
        index: number;
    };

    const handshakeSendLinkHooks: HandshakeLinkHook[] = [];
    const handshakeReceiveLinkHooks: HandshakeLinkHook[] = [];

    const compileReturnTransitionPlusPlus = function (inTransition: ReturnTransitionPlusPlus): void {
        if (inTransition.inFlows.length !== 1 || inTransition.outFlows.length !== 0) throw new Error("return transitions must have one inflow and no outflows");

        outTransitions.push({
            key: transitionNameSuggester.suggestName(inTransition.key + '-terminate'),
            displayName: inTransition.displayName + "-terminate",
            guard: 'agent.rd == 0',
            inFlows: [
                {
                    source: inTransition.inFlows[0].source.key,
                    pattern: '{ agent }'
                }
            ],
            outFlows: [
                {
                    target: agentGraveyardPlaceKey,
                    expression: 'agent.id'
                }
            ],
            extensions: {
                extraTag: mergeExtraTags(inTransition, ["return-transitions"]),
                plusplus: {
                    type: "terminate"
                }
            }
        });

        const returningPlaceKey = placeNameSuggester.suggestName(inTransition.key + '-returning');
        outPlaces.push({
            key: returningPlaceKey,
            displayName: inTransition.key + "-returning",
            extensions: {
                extraTag: runtimeTags.returningPlace 
            }
        });

        returnLinkHooks.push({
            returningPlaceKey
        });

        outTransitions.push({
            key: transitionNameSuggester.suggestName(inTransition.key),
            displayName: inTransition.displayName,
            guard: 'agent.rd > 0',
            inFlows: [
                {
                    source: inTransition.inFlows[0].source.key,
                    pattern: '{ agent, vars }'
                }
            ],
            outFlows: [
                {
                    target: returningPlaceKey,
                    expression: `{ agent, ret: eval(${inTransition.expression}, vars), vars }`
                }
            ],
            extensions: {
                extraTag: mergeExtraTags(inTransition, ["return-transitions"]),
                plusplus: {
                    type: "return-prepare"
                }
            }
        });
    };

    const compileStartAgentTransitionPlusPlus = function (inTransition: StartAgentTransitionPlusPlus): void {
        if (inTransition.inFlows.length !== 1 || inTransition.outFlows.length !== 2) throw new Error("start-agent transitions must have one inflow and two outflows");

        let argsExpression = "";
        _.each(inTransition.arguments, (argument) => {
            if (argsExpression) argsExpression += ', ';
            argsExpression += argument.name + ' : eval(' + argument.expression + ', vars)';
        });

        const calleeStartPlace = inTransition.outFlows[1].target;

        outTransitions.push({
            key: transitionNameSuggester.suggestName(inTransition.key),
            displayName: inTransition.displayName,
            guard: 'true',
            inFlows: [
                {
                    source: inTransition.inFlows[0].source.key,
                    pattern: '{ agent, vars }'
                },
                {
                    source: agentGeneratorPlaceKey,
                    pattern: 'id'
                }
            ],
            outFlows: [
                {
                    target: agentGeneratorPlaceKey,
                    expression: 'id + 1'
                },
                {
                    target: inTransition.outFlows[0].target.key,
                    expression: `{ agent, vars: { ...vars, ${inTransition.name} : id } }`
                },
                {
                    target: calleeStartPlace.key,
                    expression: `{ agent: { id, rd : 0 }, vars : { ${argsExpression} } }`
                }
            ],
            extensions: {
                extraTag: extraTagsOf(inTransition),
                plusplus: {
                    type: "start-agent"
                }
            }
        });
    };

    const compileJoinTransitionPlusPlus = function (inTransition: JoinTransitionPlusPlus): void {
        if (inTransition.inFlows.length !== 1 || inTransition.outFlows.length !== 1) throw new Error("join transitions must have one inflow and one outflow");

        outTransitions.push({
            key: transitionNameSuggester.suggestName(inTransition.key),
            displayName: inTransition.displayName,
            guard: `a == eval(${inTransition.agent}, vars)`,
            inFlows: [
                {
                    source: inTransition.inFlows[0].source.key,
                    pattern: '{ agent, vars }'
                },
                {
                    source: agentGraveyardPlaceKey,
                    pattern: 'a'
                }
            ],
            outFlows: [
                {
                    target: agentGraveyardPlaceKey,
                    expression: 'a'
                },
                {
                    target: inTransition.outFlows[0].target.key,
                    expression: '{ agent, vars }'
                }
            ],
            extensions: {
                extraTag: extraTagsOf(inTransition),
                plusplus: {
                    type: "join"
                }
            }
        });
    };

    const getProjectionExpressionForPath = function (path: string[]): string {
        return _.join(_.map(path, (pathElement) => `[eval(${pathElement}, vars)]`), '');
    };

    /**
     * Returns an expression that evaluates a path as an array.
     */
    const getPathDebugExpression = function (path?: string[]): string {
        return "[" + _.join(_.map(path ?? [], (pathElement) => `eval(${pathElement}, vars)`), ', ') + "]";
    };

    const compileGlobalReadTransitionPlusPlus = function (inTransition: GlobalReadTransitionPlusPlus): void {
        if (inTransition.inFlows.length !== 1 || inTransition.outFlows.length !== 1) throw new Error("global variable transitions must have one inflow and one outflow");

        const path = inTransition.path;

        outTransitions.push({
            key: transitionNameSuggester.suggestName(inTransition.key),
            displayName: inTransition.displayName,
            guard: 'true',
            inFlows: [
                {
                    source: inTransition.inFlows[0].source.key,
                    pattern: '{ agent, vars }'
                },
                {
                    source: globalVariablePlaceKeys[inTransition.variable],
                    pattern: 'v'
                }
            ],
            outFlows: [
                {
                    target: inTransition.outFlows[0].target.key,
                    expression: `{ agent, vars: { ...vars, ${inTransition.target} : v${getProjectionExpressionForPath(path)} } }`
                },
                {
                    target: globalVariablePlaceKeys[inTransition.variable],
                    expression: 'v'
                }
            ],
            extensions: {
                extraTag: extraTagsOf(inTransition),
                plusplus: {
                    type: "read-global",
                    variable: inTransition.variable,
                    path: getPathDebugExpression(path)
                }
            }
        });
    };

    const assembleUpdateExpressionForPath = function (path: string[], newValue: string): string {
        let res = newValue;

        if (path.length) {
            // assemble update expression, e.g. value[1 : value[1][2: value[1][2][3: 42]]]

            //                               e.g. "[1][2]"             e.g. "42"                iteration var
            const assembleValueExpression = (subvalueAccessor: string, innerExpression: string, remainingPath: string[]): string => {
                if (remainingPath.length) {
                    const pathHead = _.head(remainingPath);
                    const newSubvalueAccessor = `${subvalueAccessor}[eval(${pathHead}, vars)]`;
                    return `value${subvalueAccessor}[eval(${pathHead}, vars) : ${assembleValueExpression(newSubvalueAccessor, innerExpression, _.tail(remainingPath))}]`;
                } else {
                    return innerExpression;
                }
            };

            res = assembleValueExpression('', res, path);
        }

        return res;
    };

    const compileGlobalWriteTransitionPlusPlus = function (inTransition: GlobalWriteTransitionPlusPlus): void {
        if (inTransition.inFlows.length !== 1 || inTransition.outFlows.length !== 1) throw new Error("global variable transitions must have one inflow and one outflow");

        const path = inTransition.path;

        outTransitions.push({
            key: transitionNameSuggester.suggestName(inTransition.key),
            displayName: inTransition.displayName,
            guard: 'true',
            inFlows: [
                {
                    source: inTransition.inFlows[0].source.key,
                    pattern: '{ agent, vars }'
                },
                {
                    source: globalVariablePlaceKeys[inTransition.variable],
                    pattern: path.length ? 'value' : '_'
                }
            ],
            outFlows: [
                {
                    target: inTransition.outFlows[0].target.key,
                    expression: '{ agent, vars }'
                },
                {
                    target: globalVariablePlaceKeys[inTransition.variable],
                    expression: assembleUpdateExpressionForPath(path, `eval(${inTransition.value}, vars)`)
                }
            ],
            extensions: {
                extraTag: extraTagsOf(inTransition),
                plusplus: {
                    type: "write-global",
                    variable: inTransition.variable,
                    path: getPathDebugExpression(path)
                }
            }
        });
    };

    const compileGlobalUpdateTransitionPlusPlus = function (inTransition: GlobalUpdateTransitionPlusPlus): void {
        if (inTransition.inFlows.length !== 1 || inTransition.outFlows.length !== 1) throw new Error("global variable transitions must have one inflow and one outflow");

        const path = inTransition.path;

        outTransitions.push({
            key: transitionNameSuggester.suggestName(inTransition.key),
            displayName: inTransition.displayName,
            guard: 'true',
            inFlows: [
                {
                    source: inTransition.inFlows[0].source.key,
                    pattern: '{ agent, vars }'
                },
                {
                    source: globalVariablePlaceKeys[inTransition.variable],
                    pattern: 'value'
                }
            ],
            outFlows: [
                {
                    target: inTransition.outFlows[0].target.key,
                    expression: inTransition.target ? `{ agent, vars: { ...vars, ${inTransition.target} : value${getProjectionExpressionForPath(path)} } }` : '{ agent, vars }'
                },
                {
                    target: globalVariablePlaceKeys[inTransition.variable],
                    expression: assembleUpdateExpressionForPath(path, `eval(${inTransition.update}, { x: value${getProjectionExpressionForPath(path)}, env: vars })`)
                }
            ],
            extensions: {
                extraTag: extraTagsOf(inTransition),
                plusplus: {
                    type: "update-global",
                    variable: inTransition.variable,
                    path: getPathDebugExpression(path)
                }
            }
        });
    };

    const compileMutexInitTransitionPlusPlus = function (inTransition: MutexInitTransitionPlusPlus): void {
        if (inTransition.inFlows.length !== 1 || inTransition.outFlows.length !== 1) throw new Error("mutex transitions must have one inflow and one outflow");

        outTransitions.push({
            key: transitionNameSuggester.suggestName(inTransition.key),
            displayName: inTransition.displayName,
            guard: 'true',
            inFlows: [
                {
                    source: inTransition.inFlows[0].source.key,
                    pattern: '{ agent, vars }'
                },
                {
                    source: mutexGeneratorPlaceKey,
                    pattern: 'id'
                }
            ],
            outFlows: [
                {
                    target: inTransition.outFlows[0].target.key,
                    expression: `{ agent, vars: { ...vars, ${inTransition.mutex} : id } }`
                },
                {
                    target: mutexGeneratorPlaceKey,
                    expression: 'id + 1'
                },
                {
                    target: mutexStorePlaceKey,
                    expression: '{ id, owner: -1, count: 0 }'
                }
            ],
            extensions: {
                extraTag: extraTagsOf(inTransition),
                plusplus: {
                    type: "init-mutex"
                }
            }
        });
    };

    const compileMutexLockTransitionPlusPlus = function (inTransition: MutexLockTransitionPlusPlus): void {
        if (inTransition.inFlows.length !== 1 || inTransition.outFlows.length !== 1) throw new Error("mutex transitions must have one inflow and one outflow");

        outTransitions.push({
            key: transitionNameSuggester.suggestName(inTransition.key),
            displayName: inTransition.displayName,
            guard: `mid == eval(${inTransition.mutex}, vars) && (agent.id == owner || count == 0)`,
            inFlows: [
                {
                    source: inTransition.inFlows[0].source.key,
                    pattern: `{ agent, vars }`
                },
                {
                    source: mutexStorePlaceKey,
                    pattern: `{ id : mid, owner, count }`
                }
            ],
            outFlows: [
                {
                    target: inTransition.outFlows[0].target.key,
                    expression: `{ agent, vars }`
                },
                {
                    target: mutexStorePlaceKey,
                    expression: `{ id : mid, owner : agent.id, count : count + 1 }`
                }
            ],
            extensions: {
                extraTag: extraTagsOf(inTransition),
                plusplus: {
                    type: "lock-mutex"
                }
            }
        });
    };

    const compileMutexUnlockTransitionPlusPlus = function (inTransition: MutexUnlockTransitionPlusPlus): void {
        if (inTransition.inFlows.length !== 1 || inTransition.outFlows.length !== 1) throw new Error("mutex transitions must have one inflow and one outflow");

        outTransitions.push({
            key: transitionNameSuggester.suggestName(inTransition.key),
            displayName: inTransition.displayName,
            guard: `mid == eval(${inTransition.mutex}, vars) && agent.id == owner && count > 0`,
            inFlows: [
                {
                    source: inTransition.inFlows[0].source.key,
                    pattern: `{ agent, vars }`
                },
                {
                    source: mutexStorePlaceKey,
                    pattern: `{ id : mid, owner, count }`
                }
            ],
            outFlows: [
                {
                    target: inTransition.outFlows[0].target.key,
                    expression: `{ agent, vars }`
                },
                {
                    target: mutexStorePlaceKey,
                    expression: `{ id : mid, owner : (count > 1 ? owner : -1), count : count - 1 }`
                }
            ],
            extensions: {
                extraTag: extraTagsOf(inTransition),
                plusplus: {
                    type: "unlock-mutex"
                }
            }
        });
    };

    const compileConditionInitTransitionPlusPlus = function (inTransition: ConditionInitTransitionPlusPlus): void {
        outTransitions.push({
            key: transitionNameSuggester.suggestName(inTransition.key),
            displayName: inTransition.displayName,
            guard: 'true',
            inFlows: [
                {
                    source: inTransition.inFlows[0].source.key,
                    pattern: '{ agent, vars }'
                },
                {
                    source: conditionGeneratorPlaceKey,
                    pattern: 'id'
                }
            ],
            outFlows: [
                {
                    target: inTransition.outFlows[0].target.key,
                    expression: `{ agent, vars: { ...vars, ${inTransition.condition} : id } }`
                },
                {
                    target: conditionGeneratorPlaceKey,
                    expression: 'id + 1'
                },
                {
                    target: conditionStorePlaceKey,
                    expression: `{ mutex: eval(${inTransition.mutex}, vars), condition: id, agents: 0 }`
                }
            ],
            extensions: {
                extraTag: extraTagsOf(inTransition),
                plusplus: {
                    type: "init-condition"
                }
            }
        });
    };

    const compileConditionAwaitTransitionPlusPlus = function (inTransition: ConditionAwaitTransitionPlusPlus): void {
        const awaitingSignalPlaceKey = placeNameSuggester.suggestName(inTransition.key + "-awaiting-signal");
        const reobtainingMutexPlaceKey = placeNameSuggester.suggestName(inTransition.key + "-reobtaining-mutex");
        const extraTagInsideFalseBranch = extraTagsOf(inTransition);

        outPlaces.push({
            key: awaitingSignalPlaceKey,
            displayName: "awaiting signal",
            extensions: {
                sourcemap: inTransition.inFlows[0].source.extensions.sourcemap,
                extraTag: extraTagInsideFalseBranch,
                plusplus: {
                    type: 'condition-await-waiting-for-signal'
                }
            }
        });

        outPlaces.push({
            key: reobtainingMutexPlaceKey,
            displayName: "reobtaining mutex",
            extensions: {
                sourcemap: inTransition.inFlows[0].source.extensions.sourcemap,
                extraTag: extraTagsOf(inTransition),
                plusplus: {
                    type: 'condition-await-reobtaining-mutex'
                }
            }
        });


        outTransitions.push({
            key: transitionNameSuggester.suggestName(`${inTransition.key}-start-awaiting`),
            displayName: `${inTransition.displayName} (start awaiting)`,
            guard: `condition == eval(${inTransition.condition}, vars) && owner == agent.id`,
            inFlows: [
                {
                    source: inTransition.inFlows[0].source.key,
                    pattern: `{ agent, vars }`
                },
                {
                    source: conditionSignalRelayReadyPlaceKey, // not strictly necessary, but reduces state space
                    pattern: `{}`
                },
                {
                    source: conditionStorePlaceKey,
                    pattern: `{ mutex, condition, agents }`
                },
                {
                    source: mutexStorePlaceKey,
                    pattern: `{ id : mutex, owner, count }`
                }
            ],
            outFlows: [
                {
                    target: awaitingSignalPlaceKey,
                    expression: `{ agent, vars, condition, mutex, mutexReentrancyCount: count }`
                },
                {
                    target: conditionSignalRelayReadyPlaceKey, // not strictly necessary, but reduces state space
                    expression: `{}`
                },
                {
                    target: conditionStorePlaceKey,
                    expression: `{ mutex, condition, agents: agents + 1 }`
                },
                {
                    target: mutexStorePlaceKey,
                    expression: `{ id : mutex, owner: -1, count: 0 }`
                }
            ],
            extensions: {
                extraTag: extraTagsOf(inTransition),
                plusplus: {
                    type: "await-condition"
                }
            }
        });

        outTransitions.push({
            key: transitionNameSuggester.suggestName(`${inTransition.key}-process-signalAll`),
            displayName: `${inTransition.displayName} (processing signalAll)`,
            guard: 'signalAll',
            inFlows: [
                {
                    source: awaitingSignalPlaceKey,
                    pattern: `{ agent, vars, condition, mutex, mutexReentrancyCount }`
                },
                {
                    source: conditionSignalRelaySignalingPlaceKey,
                    pattern: `{ condition, signalAll }`
                },
                {
                    source: conditionStorePlaceKey,
                    pattern: `{ mutex, condition, agents }`
                }
            ],
            outFlows: [
                {
                    target: reobtainingMutexPlaceKey,
                    expression: `{ agent, vars, condition, mutex, mutexReentrancyCount }`
                },
                {
                    target: conditionSignalRelaySignalingPlaceKey,
                    expression: `{ condition, signalAll }`
                },
                {
                    target: conditionStorePlaceKey,
                    expression: `{ mutex, condition, agents: agents - 1 }`
                }
            ],
            extensions: {
                extraTag: mergeExtraTags(inTransition, ["await-signal"]),
                plusplus: {
                    type: "signal-condition-process-all"
                }
            }
        });
        outTransitions.push({
            key: transitionNameSuggester.suggestName(`${inTransition.key}-process-signal`),
            displayName: `${inTransition.displayName} (processing signal)`,
            guard: '!signalAll',
            inFlows: [
                {
                    source: awaitingSignalPlaceKey,
                    pattern: `{ agent, vars, condition, mutex, mutexReentrancyCount }`
                },
                {
                    source: conditionSignalRelaySignalingPlaceKey,
                    pattern: `{ condition, signalAll }`
                },
                {
                    source: conditionStorePlaceKey,
                    pattern: `{ mutex, condition, agents }`
                }
            ],
            outFlows: [
                {
                    target: reobtainingMutexPlaceKey,
                    expression: `{ agent, vars, condition, mutex, mutexReentrancyCount }`
                },
                {
                    target: conditionSignalRelayReadyPlaceKey,
                    expression: `{}`
                },
                {
                    target: conditionStorePlaceKey,
                    expression: `{ mutex, condition, agents: agents - 1 }`
                }
            ],
            extensions: {
                extraTag: mergeExtraTags(inTransition, ["await-signal"]),
                plusplus: {
                    type: "signal-condition-process-single"
                }
            }
        });

        outTransitions.push({
            key: transitionNameSuggester.suggestName(`${inTransition.key}-reobtain-mutex`),
            displayName: `${inTransition.displayName} (reobtain mutex)`,
            guard: 'oldOwner == -1 && oldCount == 0',
            inFlows: [
                {
                    source: reobtainingMutexPlaceKey,
                    pattern: `{ agent, vars, mutex, mutexReentrancyCount: count }`
                },
                {
                    source: mutexStorePlaceKey,
                    pattern: `{ id : mutex, owner: oldOwner, count: oldCount }`
                }
            ],
            outFlows: [
                {
                    target: inTransition.outFlows[0].target.key,
                    expression: `{ agent, vars }`
                },
                {
                    target: mutexStorePlaceKey,
                    expression: `{ id : mutex, owner: agent.id, count }`
                }
            ],
            extensions: {
                extraTag: extraTagsOf(inTransition),
                plusplus: {
                    type: "signal-reobtain-mutex"
                }
            }
        });
    };

    const compileConditionSignalTransitionPlusPlus = function (inTransition: ConditionSignalTransitionPlusPlus): void {
        outTransitions.push({
            key: transitionNameSuggester.suggestName(inTransition.key),
            displayName: inTransition.displayName,
            guard: 'true',
            inFlows: [
                {
                    source: inTransition.inFlows[0].source.key,
                    pattern: '{ agent, vars }'
                },
                {
                    source: conditionSignalRelayReadyPlaceKey,
                    pattern: '{}'
                }
            ],
            outFlows: [
                {
                    target: inTransition.outFlows[0].target.key,
                    expression: `{ agent, vars }`
                },
                {
                    target: conditionSignalRelaySignalingPlaceKey,
                    expression: `{ condition: eval(${inTransition.condition}, vars), signalAll: eval(${inTransition.signalAll}, vars) }`
                }
            ],
            extensions: {
                extraTag: extraTagsOf(inTransition),
                plusplus: {
                    type: "signal-condition"
                }
            }
        });
    };


    const compileInitChanTransitionPlusPlus = function (inTransition: InitChanTransitionPlusPlus): void {
        if (inTransition.inFlows.length !== 1 || inTransition.outFlows.length !== 1) throw new Error("channel initialization transitions must have one inflow and one outflow");

        if (inTransition.compiledCapacity === 0) {
            outTransitions.push({
                key: transitionNameSuggester.suggestName(inTransition.key),
                displayName: inTransition.displayName,
                guard: 'true',
                inFlows: [
                    {
                        source: inTransition.inFlows[0].source.key,
                        pattern: '{ agent, vars }'
                    },
                    {
                        source: syncChanGenPlaceKey,
                        pattern: 'id'
                    }
                ],
                outFlows: [
                    {
                        target: inTransition.outFlows[0].target.key,
                        expression: `{ agent, vars: { ...vars, ${inTransition.channel} : id } }`
                    },
                    {
                        target: syncChanGenPlaceKey,
                        expression: 'id - 1'
                    }
                ],
                extensions: {
                    extraTag: extraTagsOf(inTransition),
                    plusplus: {
                        type: "init-chan-sync"
                    }
                }
            });
        } else if (inTransition.compiledCapacity > 0) {
            outTransitions.push({
                key: transitionNameSuggester.suggestName(inTransition.key),
                displayName: inTransition.displayName,
                guard: 'true',
                inFlows: [
                    {
                        source: inTransition.inFlows[0].source.key,
                        pattern: '{ agent, vars }'
                    },
                    {
                        source: asyncChanGenPlaceKey,
                        pattern: 'id'
                    }
                ],
                outFlows: [
                    {
                        target: inTransition.outFlows[0].target.key,
                        expression: `{ agent, vars: { ...vars, ${inTransition.channel} : id } }`
                    },
                    {
                        target: asyncChanGenPlaceKey,
                        expression: 'id + 1'
                    },
                    {
                        target: asyncChanStorePlaceKey,
                        expression: `{ id, capacity : ${inTransition.capacity}, store : [] }`
                    }
                ],
                extensions: {
                    extraTag: extraTagsOf(inTransition),
                    plusplus: {
                        type: "init-chan-async"
                    }
                }
            });
        } else {
            throw new Error(`Capacity ${inTransition.capacity} is not allowed.`);
        }
    };

    type ChannelTransition = InitChanTransitionPlusPlus | SendTransitionPlusPlus | ReceiveTransitionPlusPlus | DefaultTransitionPlusPlus;

    const channelCommandTransitions: { [sourceKey: string]: ChannelTransition[] } = {}; // map from places to send-, receive- and default-transitions originating there

    // channel commands have to be compiled as a whole per place they are starting in, so this function merely groups them, to be compiled later
    const scheduleChannelCommandCompilation = function (inTransition: ChannelTransition): void {
        if (inTransition.inFlows.length !== 1 || inTransition.outFlows.length !== 1) throw new Error("channel transitions must have one inflow and one outflow");

        const sourceKey = inTransition.inFlows[0].source.key;

        if (!_.has(channelCommandTransitions, sourceKey)) channelCommandTransitions[sourceKey] = [];
        channelCommandTransitions[sourceKey].push(inTransition);
    };

    const compileTransition = function (inTransition: Transition): void {
        if (inTransition instanceof TransitionPlusPlus) {
            if (inTransition instanceof PrintLnTransitionPlusPlus)              compilePrintLnTransitionPlusPlus(inTransition);
            else if (inTransition instanceof CallTransitionPlusPlus)            compileCallTransitionPlusPlus(inTransition);
            else if (inTransition instanceof ReturnTransitionPlusPlus)          compileReturnTransitionPlusPlus(inTransition);
            else if (inTransition instanceof StartAgentTransitionPlusPlus)      compileStartAgentTransitionPlusPlus(inTransition);
            else if (inTransition instanceof JoinTransitionPlusPlus)            compileJoinTransitionPlusPlus(inTransition);
            else if (inTransition instanceof InitChanTransitionPlusPlus)        compileInitChanTransitionPlusPlus(inTransition);
            else if (inTransition instanceof SendTransitionPlusPlus)            scheduleChannelCommandCompilation(inTransition);
            else if (inTransition instanceof ReceiveTransitionPlusPlus)         scheduleChannelCommandCompilation(inTransition);
            else if (inTransition instanceof DefaultTransitionPlusPlus)         scheduleChannelCommandCompilation(inTransition);
            else if (inTransition instanceof GlobalReadTransitionPlusPlus)      compileGlobalReadTransitionPlusPlus(inTransition);
            else if (inTransition instanceof GlobalWriteTransitionPlusPlus)     compileGlobalWriteTransitionPlusPlus(inTransition);
            else if (inTransition instanceof GlobalUpdateTransitionPlusPlus)    compileGlobalUpdateTransitionPlusPlus(inTransition);
            else if (inTransition instanceof MutexInitTransitionPlusPlus)       compileMutexInitTransitionPlusPlus(inTransition);
            else if (inTransition instanceof MutexLockTransitionPlusPlus)       compileMutexLockTransitionPlusPlus(inTransition);
            else if (inTransition instanceof MutexUnlockTransitionPlusPlus)     compileMutexUnlockTransitionPlusPlus(inTransition);
            else if (inTransition instanceof ConditionInitTransitionPlusPlus)   compileConditionInitTransitionPlusPlus(inTransition);
            else if (inTransition instanceof ConditionAwaitTransitionPlusPlus)  compileConditionAwaitTransitionPlusPlus(inTransition);
            else if (inTransition instanceof ConditionSignalTransitionPlusPlus) compileConditionSignalTransitionPlusPlus(inTransition);
            else throw new Error(`The transition ${inTransition.key} (${inTransition.displayName}) cannot be compiled because this type of transition is not supported.`);
        } else {
            compileGeneralPurposeTransition(inTransition);
        }
    };

    _.each(input.transitions, compileTransition);

    // compile channel commands

    _.each(channelCommandTransitions, (transitions, placeKey) => {
        const place = input.places[placeKey]; // this is the place where our transitions start

        // we begin by adding the "commit" transition and the corresponding placed

        const committedPlaceKey = placeNameSuggester.suggestName(place.key + "-committed");
        outPlaces.push({
            key: committedPlaceKey,
            displayName: place.displayName + " (committed to sync)",
            extensions: {
                extraTag: extraTagsOf(place),
                sourcemap: place.extensions.sourcemap
            }
        });

        let offerExpression = "";
        const syncOffers: { // used to populate the extension data to help debuggers understand the state of the system
            direction: 'send' | 'receive';
            channel: string;
            value?: string;
        }[] = [];
        let hasDefault = false;
        _.each(transitions, (transition, index) => {
            // add properties to the expression to transmit all data needed

            if (transition instanceof DefaultTransitionPlusPlus) {
                // nothing to transmit
                hasDefault = true;
            } else if (transition instanceof SendTransitionPlusPlus) {
                offerExpression += `, c${index} : eval(${transition.channel}, vars), s${index} : eval(${transition.value}, vars)`;
                syncOffers.push({
                    direction: 'send',
                    channel: `c${index}`,
                    value: `s${index}`
                });
            } else if (transition instanceof ReceiveTransitionPlusPlus) {
                offerExpression += `, c${index} : eval(${transition.channel}, vars)`;
                syncOffers.push({
                    direction: 'receive',
                    channel: `c${index}`
                });
            } else {
                throw new Error("Encountered a non-channel transition while compiling channel transitions.");
            }
        });

        const offeringPlaceKey = placeNameSuggester.suggestName(place.key + "-offering-sync");
        outPlaces.push({
            key: offeringPlaceKey,
            displayName: place.displayName + " (offering to sync)",
            extensions: {
                extraTag: runtimeTags.handshake.offering,
                plusplus: {
                    type: 'offering-sync',
                    syncOffers,
                    hasDefault
                }
            }
        });

        outTransitions.push({
            key: transitionNameSuggester.suggestName('commit-to-sync'),
            displayName: "commit to sync",
            guard: 'true',
            inFlows: [
                {
                    source: placeKey,
                    pattern: '{ agent, vars }'
                }
            ],
            outFlows: [
                {
                    target: committedPlaceKey,
                    expression: '{ agent, vars }'
                },
                {
                    target: offeringPlaceKey,
                    expression: `{ agent${offerExpression} }`
                }
            ],
            extensions: {
                extraTag: extraTagsOf(place),
            }
        });

        // next up: the "synced" transitions and corresponding place

        const syncCompletedPlaceKeys = _.map(transitions, (transition, index) => {
            const syncCompletedPlaceKey = placeNameSuggester.suggestName(placeKey + "-sync-completed-" + index);

            outPlaces.push({
                key: syncCompletedPlaceKey,
                displayName: place.displayName + ` (sync completed: ${index})`,
                extensions: {
                    extraTag: runtimeTags.handshake.completed,
                    plusplus: {
                        type: 'sync-completed'
                    }
                }
            });

            const receivePattern = transition instanceof ReceiveTransitionPlusPlus ? ',  res' : '';
            const receiveExpression = transition instanceof ReceiveTransitionPlusPlus ? `, ${transition.target} : res` : '';

            outTransitions.push({
                key: transitionNameSuggester.suggestName(`synced-${index}`),
                displayName: `finalize sync: ${index}`,
                guard: 'true',
                inFlows: [
                    {
                        source: committedPlaceKey,
                        pattern: '{ agent, vars }'
                    },
                    {
                        source: syncCompletedPlaceKey,
                        pattern: `{ agent${receivePattern} }`
                    }
                ],
                outFlows: [
                    {
                        target: transition.outFlows[0].target.key,
                        expression: `{ agent, vars: { ...vars${receiveExpression} } }`
                    }
                ],
                extensions: {
                    extraTag: extraTagsOf(transition.outFlows[0].target),
                }
            });

            return syncCompletedPlaceKey;
        });

        // next, compile asynchronous sending and receiving as well as default, and collect the data needed to link handshaking later on

        _.each(transitions, (transition, index) => {
            if (transition instanceof SendTransitionPlusPlus) {
                outTransitions.push({
                    key: transitionNameSuggester.suggestName("async-chan-send"),
                    displayName: "send on async channel",
                    guard: 'bs.length < l',
                    inFlows: [
                        {
                            source: offeringPlaceKey,
                            pattern: `{ agent, c${index} : c, s${index} : s }`
                        },
                        {
                            source: asyncChanStorePlaceKey,
                            pattern: `{ id : c, capacity : l, store : bs }`
                        }
                    ],
                    outFlows: [
                        {
                            target: syncCompletedPlaceKeys[index],
                            expression: '{ agent }'
                        },
                        {
                            target: asyncChanStorePlaceKey,
                            expression: '{ id : c, capacity : l, store : bs @ [s] }'
                        }
                    ],
                    extensions: {
                        extraTag: runtimeTags.handshake.async.send,
                        plusplus: {
                            type: "send-async"
                        }
                    }
                });

                handshakeSendLinkHooks.push({
                    offeringPlaceKey,
                    syncCompletedPlaceKey: syncCompletedPlaceKeys[index],
                    index
                });
            } else if (transition instanceof ReceiveTransitionPlusPlus) {
                outTransitions.push({
                    key: transitionNameSuggester.suggestName("async-chan-receive"),
                    displayName: "receive on async channel",
                    guard: 'true',
                    inFlows: [
                        {
                            source: offeringPlaceKey,
                            pattern: `{ agent, c${index} : c }`
                        },
                        {
                            source: asyncChanStorePlaceKey,
                            pattern: `{ id : c, capacity : l, store : [b, ...br] }`
                        }
                    ],
                    outFlows: [
                        {
                            target: syncCompletedPlaceKeys[index],
                            expression: '{ agent, res : b }'
                        },
                        {
                            target: asyncChanStorePlaceKey,
                            expression: '{ id : c, capacity : l, store : br }'
                        }
                    ],
                    extensions: {
                        extraTag: runtimeTags.handshake.async.receive,
                        plusplus: {
                            type: "receive-async"
                        }
                    }
                });

                handshakeReceiveLinkHooks.push({
                    offeringPlaceKey,
                    syncCompletedPlaceKey: syncCompletedPlaceKeys[index],
                    index
                });
            } else if (transition instanceof DefaultTransitionPlusPlus) {
                outTransitions.push({
                    key: transitionNameSuggester.suggestName("default"),
                    displayName: "default",
                    guard: 'true',
                    inFlows: [
                        {
                            source: offeringPlaceKey,
                            pattern: `{ agent }`
                        }
                    ],
                    outFlows: [
                        {
                            target: syncCompletedPlaceKeys[index],
                            expression: '{ agent }'
                        }
                    ],
                    extensions: {
                        extraTag: runtimeTags.handshake.async.default,
                        plusplus: {
                            type: "default"
                        }
                    }
                });
            } else {
                throw new Error("Encountered a non-channel transition while compiling channel transitions.");
            }
        });
    });

    // link transitions

    // link call-return
    _.each(crossProduct([callLinkHooks, returnLinkHooks]), ([{ awaitingReturnPlaceKey, nextPlaceKey, returnVariable, extraTag }, { returningPlaceKey }]) => {
        outTransitions.push({
            key: transitionNameSuggester.suggestName('process-return'),
            displayName: "process-return",
            guard: 'callerAgent.id == calleeAgent.id && callerAgent.rd == calleeAgent.rd - 1',
            inFlows: [
                {
                    source: awaitingReturnPlaceKey,
                    pattern: '{ agent : callerAgent, vars }'
                },
                {
                    source: returningPlaceKey,
                    pattern: '{ agent : calleeAgent, ret }'
                },
            ],
            outFlows: [
                {
                    target: nextPlaceKey,
                    expression: `{ agent : callerAgent, vars: { ...vars, ${returnVariable} : ret } }`
                }
            ],
            extensions: {
                extraTag: mergeExtraTags({ extensions: { extraTag } }, ["returnTransitions"]),
                graphlayout: {
                    role: 'auxiliary'
                },
                plusplus: {
                    type: "return-handshake"
                }
            }
        });
    });

    // link handshaking
    _.each(crossProduct([handshakeSendLinkHooks, handshakeReceiveLinkHooks]), ([sendHook, receiveHook]) => {
        outTransitions.push({
            key: transitionNameSuggester.suggestName('process-handshake'),
            displayName: "process-handshake",
            guard: 'c < 0',
            inFlows: [
                {
                    source: sendHook.offeringPlaceKey,
                    pattern: `{ agent : senderAgent, c${sendHook.index} : c, s${sendHook.index} : val }`
                },
                {
                    source: receiveHook.offeringPlaceKey,
                    pattern: `{ agent : receiverAgent, c${receiveHook.index} : c }`
                },
            ],
            outFlows: [
                {
                    target: sendHook.syncCompletedPlaceKey,
                    expression: `{ agent : senderAgent }`
                },
                {
                    target: receiveHook.syncCompletedPlaceKey,
                    expression: '{ agent : receiverAgent, res : val }'
                }
            ],
            extensions: {
                graphlayout: {
                    role: 'auxiliary'
                },
                extraTag: runtimeTags.handshake.sync,
                plusplus: {
                    type: 'sync-handshake'
                }
            }
        });
    });

    // compile initial marking

    const placeKeysWithInitialToken = _.keys(input.initialMarking.tokens);
    if (placeKeysWithInitialToken.length !== 1) throw new Error("The net must have exactly one initial token (but has tokens in multiple places).");
    const placeKeyWithInitialToken = placeKeysWithInitialToken[0];
    const initialTokens = input.initialMarking.tokens[placeKeyWithInitialToken];
    if (initialTokens.length != 1) throw new Error("The net must have exactly one initial token (but has multiple tokens in one place).");
    const initialToken = initialTokens[0];

    const outTokens: { [placeKey: string]: TokenObject[] } = {};

    outTokens[placeKeyWithInitialToken] = [{
        color: {
            agent: {
                id: 0,
                rd: 0
            },
            vars: initialToken.color
        }
    }];

    outTokens[agentGeneratorPlaceKey] = [{
        color: 1
    }];

    outTokens[asyncChanGenPlaceKey] = [{
        color: 1
    }];

    outTokens[syncChanGenPlaceKey] = [{
        color: -1
    }];

    outTokens[mutexGeneratorPlaceKey] = [{
        color: 1
    }];

    outTokens[conditionGeneratorPlaceKey] = [{
        color: 1
    }];

    outTokens[conditionSignalRelayReadyPlaceKey] = [{
        color: {}
    }];

    _.each(globalVariablePlaceKeys, (globalVariablePlaceKey, variableName) => {
        outTokens[globalVariablePlaceKey] = [{
            color: _.get(input.extensions, `plusplus.globalVariableInitialValues.${variableName}`, 0)
        }];
    });

    const outMarking = { tokens: outTokens, extensions: {} };

    // finalize net

    const output: PetriNetObject = {
        places: outPlaces,
        transitions: outTransitions,
        initialMarking: outMarking,
        extensions: _.merge(_.cloneDeep(input.extensions), {
            generator: "cpn-plusplus-compiler"
        })
    };

    return PetriNet.fromObject(output);
};


export {
    compile
};