{
  "code": null,
  "collection": "architecture",
  "href": "https://banes-lab.com/ontology#architecture-petri-nets",
  "id": "petri-nets",
  "kind": "model",
  "layer": {
    "href": "https://banes-lab.com/ontology/schema#layer-atomic-boundary",
    "json": "https://banes-lab.com/json/records/layer/atomic-boundary",
    "label": "Atomic Boundary",
    "markdown": "https://banes-lab.com/records/layer/atomic-boundary.md",
    "ref": "layer:atomic-boundary"
  },
  "name": "Petri Nets",
  "ref": "architecture:petri-nets",
  "relations": [
    {
      "links": [
        {
          "href": "https://banes-lab.com/ontology/lexicon#lexicon-places-and-transitions",
          "json": "https://banes-lab.com/json/records/lexicon/places-and-transitions",
          "label": "Places and Transitions",
          "markdown": "https://banes-lab.com/records/lexicon/places-and-transitions.md",
          "ref": "lexicon:places-and-transitions"
        }
      ],
      "relation": "requires"
    },
    {
      "links": [
        {
          "href": "https://banes-lab.com/ontology/lexicon#lexicon-concurrency-correctness",
          "json": "https://banes-lab.com/json/records/lexicon/concurrency-correctness",
          "label": "Concurrency Correctness",
          "markdown": "https://banes-lab.com/records/lexicon/concurrency-correctness.md",
          "ref": "lexicon:concurrency-correctness"
        },
        {
          "href": "https://banes-lab.com/ontology/lexicon#lexicon-deadlock-freedom",
          "json": "https://banes-lab.com/json/records/lexicon/deadlock-freedom",
          "label": "Deadlock Freedom",
          "markdown": "https://banes-lab.com/records/lexicon/deadlock-freedom.md",
          "ref": "lexicon:deadlock-freedom"
        }
      ],
      "relation": "reinforces"
    },
    {
      "links": [
        {
          "href": "https://banes-lab.com/ontology/lexicon#lexicon-concurrent-flow-modeling",
          "json": "https://banes-lab.com/json/records/lexicon/concurrent-flow-modeling",
          "label": "Concurrent-Flow Modeling",
          "markdown": "https://banes-lab.com/records/lexicon/concurrent-flow-modeling.md",
          "ref": "lexicon:concurrent-flow-modeling"
        },
        {
          "href": "https://banes-lab.com/ontology/lexicon#lexicon-reachability-and-deadlock-analysis",
          "json": "https://banes-lab.com/json/records/lexicon/reachability-and-deadlock-analysis",
          "label": "Reachability and Deadlock Analysis",
          "markdown": "https://banes-lab.com/records/lexicon/reachability-and-deadlock-analysis.md",
          "ref": "lexicon:reachability-and-deadlock-analysis"
        }
      ],
      "relation": "enables"
    },
    {
      "links": [
        {
          "href": "https://banes-lab.com/ontology/lexicon#lexicon-ad-hoc-lock-ordering",
          "json": "https://banes-lab.com/json/records/lexicon/ad-hoc-lock-ordering",
          "label": "Ad-Hoc Lock Ordering",
          "markdown": "https://banes-lab.com/records/lexicon/ad-hoc-lock-ordering.md",
          "ref": "lexicon:ad-hoc-lock-ordering"
        }
      ],
      "relation": "conflicts-with"
    },
    {
      "links": [
        {
          "href": "https://banes-lab.com/ontology/lexicon#lexicon-modeling-overhead",
          "json": "https://banes-lab.com/json/records/lexicon/modeling-overhead",
          "label": "Modeling Overhead",
          "markdown": "https://banes-lab.com/records/lexicon/modeling-overhead.md",
          "ref": "lexicon:modeling-overhead"
        }
      ],
      "relation": "tensions-with"
    },
    {
      "links": [
        {
          "href": "https://banes-lab.com/ontology/schema#tension-modeling-overhead-petri-nets",
          "json": "https://banes-lab.com/json/records/tension/modeling-overhead-petri-nets",
          "label": "Petri Nets / Modeling Overhead",
          "markdown": "https://banes-lab.com/records/tension/modeling-overhead-petri-nets.md",
          "ref": "tension:modeling-overhead-petri-nets"
        }
      ],
      "relation": "tensions"
    },
    {
      "links": [
        {
          "href": "https://banes-lab.com/ontology/algorithms#algorithms-petri-nets",
          "json": "https://banes-lab.com/json/records/algorithms/petri-nets",
          "label": "Petri Nets",
          "markdown": "https://banes-lab.com/records/algorithms/petri-nets.md",
          "ref": "algorithms:petri-nets"
        }
      ],
      "relation": "contracts"
    },
    {
      "links": [
        {
          "href": "https://banes-lab.com/ontology/lexicon#lexicon-ad-hoc-lock-ordering",
          "json": "https://banes-lab.com/json/records/lexicon/ad-hoc-lock-ordering",
          "label": "Ad-Hoc Lock Ordering",
          "markdown": "https://banes-lab.com/records/lexicon/ad-hoc-lock-ordering.md",
          "ref": "lexicon:ad-hoc-lock-ordering"
        }
      ],
      "relation": "violated-by"
    },
    {
      "links": [
        {
          "href": "https://banes-lab.com/ontology/schema#vocabulary-severity-contextual",
          "json": "https://banes-lab.com/json/records/vocabulary/severity-contextual",
          "label": "contextual",
          "markdown": "https://banes-lab.com/records/vocabulary/severity-contextual.md",
          "ref": "vocabulary:severity-contextual"
        }
      ],
      "relation": "severity"
    },
    {
      "links": [
        {
          "href": "https://banes-lab.com/ontology#architecture-category-transactions-state-concurrency",
          "json": "https://banes-lab.com/json/records/architecture-category/transactions-state-concurrency",
          "label": "Transactions / State / Concurrency",
          "markdown": "https://banes-lab.com/records/architecture-category/transactions-state-concurrency.md",
          "ref": "architecture-category:transactions-state-concurrency"
        }
      ],
      "relation": "category"
    },
    {
      "links": [
        {
          "href": "https://banes-lab.com/ontology/lexicon#lexicon-category-transactions-state-concurrency",
          "json": "https://banes-lab.com/json/ontology/lexicon/lexicon-category-transactions-state-concurrency",
          "label": "Transactions / State / Concurrency",
          "markdown": "https://banes-lab.com/ontology/lexicon/lexicon-category-transactions-state-concurrency.md",
          "ref": "chapter:/ontology/lexicon#lexicon-category-transactions-state-concurrency"
        },
        {
          "href": "https://banes-lab.com/ontology/algorithms#algorithms-domain-architecture",
          "json": "https://banes-lab.com/json/ontology/algorithms/algorithms-domain-architecture",
          "label": "Architecture",
          "markdown": "https://banes-lab.com/ontology/algorithms/algorithms-domain-architecture.md",
          "ref": "chapter:/ontology/algorithms#algorithms-domain-architecture"
        },
        {
          "href": "https://banes-lab.com/ontology/schema#the-vocabulary-severity",
          "json": "https://banes-lab.com/json/ontology/schema/the-vocabulary-severity",
          "label": "Severity levels",
          "markdown": "https://banes-lab.com/ontology/schema/the-vocabulary-severity.md",
          "ref": "chapter:/ontology/schema#the-vocabulary-severity"
        },
        {
          "href": "https://banes-lab.com/ontology/schema#the-resolutions",
          "json": "https://banes-lab.com/json/ontology/schema/the-resolutions",
          "label": "The resolutions",
          "markdown": "https://banes-lab.com/ontology/schema/the-resolutions.md",
          "ref": "chapter:/ontology/schema#the-resolutions"
        }
      ],
      "relation": "linked-from"
    }
  ],
  "summary": "A conceptual representation of concurrent flow as places holding tokens and transitions that consume and produce them, which can be analyzed for deadlock.",
  "siblings": {
    "next": null,
    "previous": {
      "href": "https://banes-lab.com/ontology#architecture-controlled-side-effects",
      "json": "https://banes-lab.com/json/records/architecture/controlled-side-effects",
      "label": "Controlled Side Effects",
      "markdown": "https://banes-lab.com/records/architecture/controlled-side-effects.md",
      "ref": "architecture:controlled-side-effects"
    }
  },
  "up": {
    "href": null,
    "json": "https://banes-lab.com/json/api/records/architecture",
    "label": "Architecture principles",
    "markdown": "https://banes-lab.com/api/records/architecture.md",
    "ref": "api:records/architecture"
  },
  "aliases": [],
  "exemplar": {
    "after": "const net = petriNet({\n  places: { idle: 1, aHeld: 0, bHeld: 0 },\n  transitions: [\n    { name: \"takeA\", consume: { idle: 1 }, produce: { aHeld: 1 } },\n    { name: \"takeB\", consume: { aHeld: 1 }, produce: { bHeld: 1 } },\n  ],\n});\nassertNoDeadlock(reachableMarkings(net));",
    "before": "acquire(a); acquire(b); work(); release(b); release(a);",
    "lang": "ts",
    "medium": "code"
  },
  "formedBy": null,
  "scope": [
    "concurrency",
    "workflow",
    "verification"
  ],
  "severity": "contextual"
}