{
 "cells": [
  {
   "metadata": {},
   "cell_type": "code",
   "outputs": [],
   "execution_count": null,
   "source": [
    "import warnings\n",
    "warnings.filterwarnings(\"ignore\", category=UserWarning)"
   ],
   "id": "975ee68399dd1b3d"
  },
  {
   "cell_type": "markdown",
   "id": "5279e90c",
   "metadata": {},
   "source": [
    "# Managing Process Models\n",
    "\n",
    "This tutorial will go through the steps necessary to import and manage process models.\n",
    "\n",
    "## The `LTLModel` class\n",
    "\n",
    "An LTLModel can be created from a Linear Temporal Logic on finite traces (LTLf) formula in a string format provided by the user. We adopted the LTLf syntax [here](http://ltlf2dfa.diag.uniroma1.it/ltlf_syntax). Therefore, the `LTLModel` has to be imported from `src.Declare4Py.ProcessModels.LTLModel` and then instantiated."
   ]
  },
  {
   "cell_type": "code",
   "id": "8b6c9e04",
   "metadata": {
    "ExecuteTime": {
     "end_time": "2026-05-29T13:48:51.864022100Z",
     "start_time": "2026-05-29T13:48:50.257056500Z"
    }
   },
   "source": [
    "from Declare4Py.ProcessModels.LTLModel import LTLModel\n",
    "\n",
    "model = LTLModel()\n",
    "model.parse_from_string(\"G(ER Triage -> F(CRP))\")"
   ],
   "outputs": [],
   "execution_count": 1
  },
  {
   "cell_type": "code",
   "id": "c99e909c",
   "metadata": {
    "ExecuteTime": {
     "end_time": "2026-05-29T13:48:51.913528200Z",
     "start_time": "2026-05-29T13:48:51.865022900Z"
    }
   },
   "source": [
    "from ltlf2dfa.parser.ltlf import LTLfParser\n",
    "\n",
    "parser = LTLfParser()\n",
    "formula_str = \"G(a -> WX b)\"\n",
    "formula = parser(formula_str)       # returns an LTLfFormula\n",
    "\n",
    "print(formula)   "
   ],
   "outputs": [
    {
     "name": "stdout",
     "output_type": "stream",
     "text": [
      "G((a -> WX(b)))\n"
     ]
    }
   ],
   "execution_count": 2
  },
  {
   "cell_type": "markdown",
   "id": "94911ff3",
   "metadata": {},
   "source": [
    "Some basic logical operations on the formulas can be done according to the methods in the `LTLModel` class. We provide some examples."
   ]
  },
  {
   "cell_type": "code",
   "id": "2cb06709",
   "metadata": {
    "ExecuteTime": {
     "end_time": "2026-05-29T13:48:51.933528400Z",
     "start_time": "2026-05-29T13:48:51.915528700Z"
    }
   },
   "source": [
    "model.parse_from_string(\"CRP\")\n",
    "\n",
    "model.add_eventually()\n",
    "print(model.formula)\n",
    "model.add_negation()\n",
    "print(model.formula)\n",
    "model.add_implication(\"F(Release A)\")\n",
    "print(model.formula)\n",
    "print(\"--------------------------------\\n\")\n",
    "\n",
    "model.parse_from_string(\"Leucocytes\")\n",
    "print(model.formula)\n",
    "model.add_until(\"!(CRP)\")\n",
    "print(model.formula)\n",
    "model.add_always()\n",
    "print(model.formula)\n",
    "print(\"--------------------------------\\n\")\n",
    "\n",
    "model.parse_from_string(\"IV Liquid\")\n",
    "print(model.formula)\n",
    "model.add_disjunction(\"IV Antibiotics\")\n",
    "print(model.formula)\n",
    "model.add_conjunction(\"X[!](Admission NC)\")\n",
    "print(model.formula)\n",
    "print(\"--------------------------------\\n\")\n",
    "\n",
    "model.parse_from_string(\"Return ER\")\n",
    "print(model.formula)\n",
    "model.add_next()\n",
    "print(model.formula)\n",
    "model.add_equivalence(\"Bad condition\")\n",
    "print(model.formula)"
   ],
   "outputs": [
    {
     "name": "stdout",
     "output_type": "stream",
     "text": [
      "F(crp)\n",
      "!(F(crp))\n",
      "(!(F(crp))) -> (F(releasea))\n",
      "--------------------------------\n",
      "\n",
      "leucocytes\n",
      "(leucocytes) U (!(crp))\n",
      "G((leucocytes) U (!(crp)))\n",
      "--------------------------------\n",
      "\n",
      "ivliquid\n",
      "(ivliquid) || (ivantibiotics)\n",
      "((ivliquid) || (ivantibiotics)) && (X[!](admissionnc))\n",
      "--------------------------------\n",
      "\n",
      "returner\n",
      "X[!](returner)\n",
      "(X[!](returner)) <-> (badcondition)\n"
     ]
    }
   ],
   "execution_count": 3
  },
  {
   "cell_type": "code",
   "id": "cb3f5191",
   "metadata": {
    "ExecuteTime": {
     "end_time": "2026-05-29T13:48:52.946728500Z",
     "start_time": "2026-05-29T13:48:51.935528500Z"
    }
   },
   "source": [
    "from logaut import ltl2dfa\n",
    "model.parse_from_string(\"!(X[!](true))\") # si usa parse_ltl da pylogics.parsers\n",
    "print(model.formula)\n",
    "print(model.parsed_formula)\n",
    "model.check_satisfiability()\n",
    "dfa1 = ltl2dfa(model.parsed_formula, backend=\"lydia\")\n",
    "dfa1 = dfa1.minimize()\n",
    "print(dfa1.__dict__)\n",
    "print(dfa1.accepts([{'a': True}, {'a': True}]))\n",
    "print(\"-------\")\n",
    "\n",
    "#dfa = ltl2dfa(model.parsed_formula, backend=\"ltlf2dfa\")\n",
    "#dfa = dfa.minimize()\n",
    "#print(dfa.__dict__)\n",
    "#print(dfa.accepts([{'a': True}, {'a': True}]))"
   ],
   "outputs": [
    {
     "name": "stdout",
     "output_type": "stream",
     "text": [
      "!(X[!](true))\n",
      "(not (next PropositionalTrue(Logic.LTL)))\n",
      "{'_state_attributes': {}, '_transition_attributes': {}, '_initial_state': 0, '_states': {0, 1, 2}, '_final_states': {0, 1}, '_state_counter': 3, '_transition_function': {0: {1: True}, 2: {2: True}, 1: {2: True}}}\n",
      "False\n",
      "-------\n"
     ]
    }
   ],
   "execution_count": 4
  },
  {
   "cell_type": "markdown",
   "id": "7f8af065",
   "metadata": {},
   "source": [
    "### Checking an LTLf model satisfiability\n",
    "\n",
    "An LTLf model can be checked according to its satisfiability (i.e., whether it is satisfiable by a trace or not) with the `check_satisfiability` method. This is done by transforming the LTLf formula into a Deterministic Finite state Automaton (DFA) and checking its emptyness. This transformation is performed by using two backends:\n",
    "\n",
    " - Lydia, C++ backend that needs to be installed with Docker, more details [here](https://github.com/whitemech/logaut/tree/main);\n",
    " - LTLf2DFA, that needs to be installed with `pip install git+https://github.com/whitemech/LTLf2DFA.git@develop#egg=ltlf2dfa`. More details [here](https://github.com/whitemech/LTLf2DFA/).\n",
    " \n",
    "Declare4Py provides the `to_ltlf2dfa_backend` and `to_lydia_backend` methods to switch the backends of the LTLf model. The default backend is Lydia.\n",
    "\n",
    "The `check_satisfiability` method takes as input the `minimize_automaton` boolean parameter (with `True` as default) that performs the minimization of the resulting DFA before the satisfiability checking."
   ]
  },
  {
   "cell_type": "code",
   "id": "beece8db",
   "metadata": {
    "ExecuteTime": {
     "end_time": "2026-05-29T13:48:53.948940700Z",
     "start_time": "2026-05-29T13:48:52.982031300Z"
    }
   },
   "source": [
    "model.parse_from_string(\"CRP & X[!](F(ER Triage && X[!](F(Admission NC))))\")\n",
    "print(f\"{model.formula} is satisfiable? {model.check_satisfiability()}\")\n",
    "\n",
    "model.parse_from_string(\"G(CRP) && F(!(CRP))\")\n",
    "print(f\"{model.formula} is satisfiable? {model.check_satisfiability(minimize_automaton=False)}\" )\n",
    "\n",
    "#model.to_ltlf2dfa_backend()\n",
    "#model.parse_from_string(\"CRP & X(F(ER Triage && X(F(Admission NC))))\")\n",
    "#print(f\"{model.formula} is satisfiable? {model.check_satisfiability()}\")"
   ],
   "outputs": [
    {
     "name": "stdout",
     "output_type": "stream",
     "text": [
      "crp &X[!](F(ertriage  && X[!](F(admissionnc)))) is satisfiable? True\n",
      "G(crp)  && F(!(crp)) is satisfiable? False\n"
     ]
    }
   ],
   "execution_count": 5
  },
  {
   "cell_type": "markdown",
   "id": "ae747b9e",
   "metadata": {},
   "source": [
    "### The `LTLTemplate` class\n",
    "\n",
    "The `LTLTemplate` class in `src.Declare4Py.ProcessModels.LTLModel` provides a set of useful LTLf templates. This set contains simple LTLf templates and [Target-Branched DECLARE templates](https://www.sciencedirect.com/science/article/pii/S0306437915001271). Here, we just list them and their corresponding LTLf formulas. A more detailed use will be shown in the tutorial of the conformance checking with LTLf models.\n",
    "\n",
    "An LTLf template can be instantiated by providing the name of the template to the `LTLTemplate` class. Then, the template has to be filled with proper activity names with the `fill_template()` method:"
   ]
  },
  {
   "cell_type": "code",
   "id": "6dec85fe",
   "metadata": {
    "ExecuteTime": {
     "end_time": "2026-05-29T13:48:53.996904500Z",
     "start_time": "2026-05-29T13:48:53.964888400Z"
    }
   },
   "source": [
    "from Declare4Py.ProcessModels.LTLModel import LTLTemplate\n",
    "\n",
    "template = LTLTemplate('eventually_a_then_b')\n",
    "model = template.fill_template(['Leucocytes', 'CRP'])\n",
    "print(f\"Formula for {template.template_str}: {model.formula}\")"
   ],
   "outputs": [
    {
     "name": "stdout",
     "output_type": "stream",
     "text": [
      "Formula for eventually_a_then_b: F(con_leucocytes  && F(con_crp))\n"
     ]
    }
   ],
   "execution_count": 6
  },
  {
   "cell_type": "markdown",
   "id": "607ed54d",
   "metadata": {},
   "source": [
    "Declare4Py provides the following set of simple LTLf templates:\n",
    "\n",
    "1. `next_a`;\n",
    "2. `eventually_a`;\n",
    "3. `eventually_a_and_eventually_b`;\n",
    "4. `eventually_a_then_b`;\n",
    "5. `eventually_a_or_b`;\n",
    "6. `eventually_a_next_b`;\n",
    "7. `eventually_a_then_b_then_c`;\n",
    "8. `eventually_a_next_b_next_c`;\n",
    "\n",
    "the following set of LTLf templates called Is First (Last):\n",
    "\n",
    "1. `is_first_state_a`;\n",
    "2. `is_second_state_a`;\n",
    "3. `is_third_state_a`;\n",
    "4. `last`;\n",
    "5. `second_last`;\n",
    "6. `third_last`;\n",
    "7. `is_last_state_a`;\n",
    "8. `is_second_last_state_a`;\n",
    "9. `is_third_last_state_a`;\n",
    "\n",
    "the following set of LTLf templates with multiple attributes:\n",
    "\n",
    "1. `p_does_a`;\n",
    "2. `a_is_done_by_p_and_q`;\n",
    "3. `p_does_a_and_b`;\n",
    "4. `p_does_a_and_then_b`;\n",
    "5. `p_does_a_and_eventually_b`;\n",
    "6. `p_does_a_a_not_b`;\n",
    "7. `a_done_by_p_p_not_q`;\n",
    "\n",
    "and the following [Target-Branched DECLARE templates](https://www.sciencedirect.com/science/article/pii/S0306437915001271):\n",
    "\n",
    "1. `precedence`;\n",
    "2. `chain_precedence`;\n",
    "3. `responded_existence`;\n",
    "4. `chain_response`;\n",
    "5. `not_chain_precedence`;\n",
    "6. `not_chain_response`;\n",
    "7. `response`;\n",
    "8. `not_precedence`;\n",
    "9. `not_response`;\n",
    "10. `not_responded_existence`;\n",
    "11. `alternate_response`;\n",
    "12. `alternate_precedence`.\n",
    "\n",
    "We show the corresponding LTLf formulas of the templates."
   ]
  },
  {
   "cell_type": "code",
   "id": "bb466a45",
   "metadata": {
    "ExecuteTime": {
     "end_time": "2026-05-29T13:48:54.041306400Z",
     "start_time": "2026-05-29T13:48:53.999540400Z"
    }
   },
   "source": [
    "from Declare4Py.ProcessModels.LTLModel import LTLTemplate\n",
    "\n",
    "print(\"\\nSimple LTLf templates:\")\n",
    "print(\"---------------------\")\n",
    "template = LTLTemplate('next_a')\n",
    "model = template.fill_template(['ER Triage'])\n",
    "print(f\"Formula for {template.template_str}: {model.formula}\")\n",
    "\n",
    "template: LTLTemplate = LTLTemplate('eventually_a')\n",
    "model: LTLModel = template.fill_template(['CRP'])\n",
    "print(f\"Formula for {template.template_str}: {model.formula}\")\n",
    "\n",
    "template = LTLTemplate('eventually_a_then_b')\n",
    "model = template.fill_template(['Leucocytes', 'CRP'])\n",
    "print(f\"Formula for {template.template_str}: {model.formula}\")\n",
    "\n",
    "template = LTLTemplate('eventually_a_or_b')\n",
    "model = template.fill_template(['Leucocytes', 'CRP'])\n",
    "print(f\"Formula for {template.template_str}: {model.formula}\")\n",
    "\n",
    "template = LTLTemplate('eventually_a_next_b')\n",
    "model = template.fill_template(['Leucocytes', 'CRP'])\n",
    "print(f\"Formula for {template.template_str}: {model.formula}\")\n",
    "\n",
    "template = LTLTemplate('eventually_a_then_b_then_c')\n",
    "model = template.fill_template(['ER Registration', 'Leucocytes', 'CRP'])\n",
    "print(f\"Formula for {template.template_str}: {model.formula}\")\n",
    "\n",
    "template = LTLTemplate('eventually_a_next_b_next_c')\n",
    "model = template.fill_template(['ER Registration', 'CRP', 'Leucocytes'])\n",
    "print(f\"Formula for {template.template_str}: {model.formula}\")\n",
    "\n",
    "print(\"\\nIs First (Last) LTLf templates:\")\n",
    "print(\"---------------------\")\n",
    "\n",
    "template = LTLTemplate('is_first_state_a')\n",
    "model = template.fill_template(['ER Triage'])\n",
    "print(f\"Formula for {template.template_str}: {model.formula}\")\n",
    "\n",
    "template: LTLTemplate = LTLTemplate('is_second_state_a')\n",
    "model: LTLModel = template.fill_template(['CRP'])\n",
    "print(f\"Formula for {template.template_str}: {model.formula}\")\n",
    "\n",
    "template = LTLTemplate('is_third_state_a')\n",
    "model = template.fill_template(['Leucocytes'])\n",
    "print(f\"Formula for {template.template_str}: {model.formula}\")\n",
    "\n",
    "template = LTLTemplate('last')\n",
    "model = template.fill_template([])\n",
    "print(f\"Formula for {template.template_str}: {model.formula}\")\n",
    "\n",
    "template = LTLTemplate('second_last')\n",
    "model = template.fill_template([])\n",
    "print(f\"Formula for {template.template_str}: {model.formula}\")\n",
    "\n",
    "template = LTLTemplate('third_last')\n",
    "model = template.fill_template([])\n",
    "print(f\"Formula for {template.template_str}: {model.formula}\")\n",
    "\n",
    "template = LTLTemplate('is_last_state_a')\n",
    "model = template.fill_template(['ER Registration'])\n",
    "print(f\"Formula for {template.template_str}: {model.formula}\")\n",
    "\n",
    "template = LTLTemplate('is_second_last_state_a')\n",
    "model = template.fill_template(['Leucocytes'])\n",
    "print(f\"Formula for {template.template_str}: {model.formula}\")\n",
    "\n",
    "template = LTLTemplate('is_third_last_state_a')\n",
    "model = template.fill_template(['CRP'])\n",
    "print(f\"Formula for {template.template_str}: {model.formula}\")\n",
    "\n",
    "print(\"\\n Multiple attributes LTLf templates:\")\n",
    "print(\"---------------------\")\n",
    "template = LTLTemplate('p_does_a')\n",
    "model = template.fill_template(['A', 'ER Registration'], attr_type=['org:group', 'concept:name'])\n",
    "print(f\"Formula for {template.template_str}: {model.formula}\")\n",
    "\n",
    "template: LTLTemplate = LTLTemplate('a_is_done_by_p_and_q')\n",
    "model: LTLModel = template.fill_template(['A', 'B', 'ER Registration'], attr_type=['org:group', 'concept:name'])\n",
    "print(f\"Formula for {template.template_str}: {model.formula}\")\n",
    "\n",
    "template = LTLTemplate('p_does_a_and_b')\n",
    "model = template.fill_template(['A', 'ER Registration', 'Leucocytes'], attr_type=['org:group', 'concept:name'])\n",
    "print(f\"Formula for {template.template_str}: {model.formula}\")\n",
    "\n",
    "template = LTLTemplate('p_does_a_and_then_b')\n",
    "model = template.fill_template(['A', 'ER Registration', 'Leucocytes'], attr_type=['org:group', 'concept:name'])\n",
    "print(f\"Formula for {template.template_str}: {model.formula}\")\n",
    "\n",
    "template = LTLTemplate('p_does_a_and_eventually_b')\n",
    "model = template.fill_template(['A', 'ER Registration', 'Leucocytes'], attr_type=['org:group', 'concept:name'])\n",
    "print(f\"Formula for {template.template_str}: {model.formula}\")\n",
    "\n",
    "template = LTLTemplate('p_does_a_a_not_b')\n",
    "model = template.fill_template(['A', 'ER Registration', 'Leucocytes'], attr_type=['org:group', 'concept:name'])\n",
    "print(f\"Formula for {template.template_str}: {model.formula}\")\n",
    "\n",
    "template = LTLTemplate('a_done_by_p_p_not_q')\n",
    "model = template.fill_template(['A', 'B', 'ER Registration'], attr_type=['org:group', 'concept:name'])\n",
    "print(f\"Formula for {template.template_str}: {model.formula}\")\n",
    "\n",
    "\n",
    "print(\"\\nTB-DECLARE templates:\")\n",
    "print(\"---------------------\")\n",
    "tb_declare_templates = ['precedence', 'chain_precedence', 'responded_existence', 'chain_response',\n",
    "                        'not_chain_precedence', 'not_chain_response', 'response', 'not_precedence', 'not_response',\n",
    "                        'not_responded_existence', 'alternate_response', 'alternate_precedence']\n",
    "\n",
    "\n",
    "for template_str in tb_declare_templates:\n",
    "    template = LTLTemplate(template_str)\n",
    "    activation_list = [\"ER Triage\", \"CRP\"]\n",
    "    target_list = [\"Leucocytes\", \"Release A\"]\n",
    "    model = template.fill_template(activation_list, target_list)\n",
    "    print(f\"Formula for {template.template_str}: {model.formula}\")"
   ],
   "outputs": [
    {
     "name": "stdout",
     "output_type": "stream",
     "text": [
      "\n",
      "Simple LTLf templates:\n",
      "---------------------\n",
      "Formula for next_a: X[!](con_ertriage)\n",
      "Formula for eventually_a: F(con_crp)\n",
      "Formula for eventually_a_then_b: F(con_leucocytes  && F(con_crp))\n",
      "Formula for eventually_a_or_b: F(con_leucocytes) || F(con_crp)\n",
      "Formula for eventually_a_next_b: F(con_leucocytes  && X[!](con_crp))\n",
      "Formula for eventually_a_then_b_then_c: F(con_erregistration  && F(con_leucocytes  && F(con_crp)))\n",
      "Formula for eventually_a_next_b_next_c: F(con_erregistration  && X[!](con_crp  && X[!](con_leucocytes)))\n",
      "\n",
      "Is First (Last) LTLf templates:\n",
      "---------------------\n",
      "Formula for is_first_state_a: con_ertriage\n",
      "Formula for is_second_state_a: X[!](con_crp)\n",
      "Formula for is_third_state_a: X[!](X[!](con_leucocytes))\n",
      "Formula for last: !(X[!](true))\n",
      "Formula for second_last: X[!](!(X[!](true)))\n",
      "Formula for third_last: X[!](X[!](!(X[!](true))))\n",
      "Formula for is_last_state_a: F(con_erregistration  &&  !(X[!](true)))\n",
      "Formula for is_second_last_state_a: F(con_leucocytes  && X[!](!(X[!](true))))\n",
      "Formula for is_third_last_state_a: F(con_crp  && X[!](X[!](!(X[!](true)))))\n",
      "\n",
      " Multiple attributes LTLf templates:\n",
      "---------------------\n",
      "Formula for p_does_a: F(org_a  && con_erregistration)\n",
      "Formula for a_is_done_by_p_and_q: (F(F(org_a  && con_erregistration))  && F(F(org_b  && con_erregistration)))\n",
      "Formula for p_does_a_and_b: (F(F(org_a  &&  con_erregistration))  && F(F(org_a  &&  con_leucocytes)))\n",
      "Formula for p_does_a_and_then_b: F((F(org_a  && con_erregistration)  && X[!](F(org_a  && con_leucocytes))))\n",
      "Formula for p_does_a_and_eventually_b: F((F(org_a  && con_erregistration)  && F(F(org_a  && con_leucocytes))))\n",
      "Formula for p_does_a_a_not_b: F((con_erregistration  &&  (!con_leucocytes  && org_a)))\n",
      "Formula for a_done_by_p_p_not_q: F((org_a  &&   (!org_b  && con_erregistration)))\n",
      "\n",
      "TB-DECLARE templates:\n",
      "---------------------\n",
      "Formula for precedence: ((!(con_leucocytes || con_releasea))U(con_ertriage || con_crp)) || G(!(con_leucocytes || con_releasea))\n",
      "Formula for chain_precedence: G(X[!](con_leucocytes || con_releasea) ->  (con_ertriage || con_crp))\n",
      "Formula for responded_existence: F(con_ertriage || con_crp) -> F(con_leucocytes || con_releasea)\n",
      "Formula for chain_response: G((con_ertriage  || con_crp) -> X[!](con_leucocytes || con_releasea))\n",
      "Formula for not_chain_precedence: G(X[!](con_leucocytes || con_releasea) ->  !(con_ertriage || con_crp))\n",
      "Formula for not_chain_response: G((con_ertriage || con_crp) -> X[!](!(con_leucocytes || con_releasea)))\n",
      "Formula for response: G((con_ertriage || con_crp) -> F(con_leucocytes || con_releasea))\n",
      "Formula for not_precedence: G(F(con_leucocytes || con_releasea) -> !(con_ertriage || con_crp))\n",
      "Formula for not_response: G((con_ertriage || con_crp) ->  !(F(con_leucocytes || con_releasea)))\n",
      "Formula for not_responded_existence: F(con_ertriage || con_crp) ->  !(F(con_leucocytes || con_releasea))\n",
      "Formula for alternate_response: G((con_ertriage || con_crp) -> X[!]((!(con_ertriage || con_crp)U(con_leucocytes || con_releasea))))\n",
      "Formula for alternate_precedence: ((!(con_leucocytes || con_releasea))U(con_ertriage || con_crp))  && G((con_leucocytes || con_releasea) -> X[!]((!(con_leucocytes || con_releasea))U(con_ertriage || con_crp)) || G(!(con_leucocytes || con_releasea)))\n"
     ]
    }
   ],
   "execution_count": 7
  },
  {
   "cell_type": "markdown",
   "id": "1225a100",
   "metadata": {},
   "source": [
    "## The `DeclareModel` and `DeclareModelTemplate` classes\n",
    "\n",
    "The DECLARE language provides a set of LTLf templates that are well known and adopted in the Process Mininig community. We start by importing the classes `DeclareModel` and `DeclareModelTemplate`."
   ]
  },
  {
   "cell_type": "code",
   "id": "e5ae55fa",
   "metadata": {
    "ExecuteTime": {
     "end_time": "2026-05-29T13:48:54.056107400Z",
     "start_time": "2026-05-29T13:48:54.042903300Z"
    }
   },
   "source": [
    "import os\n",
    "\n",
    "from Declare4Py.ProcessModels.DeclareModel import DeclareModel\n",
    "from Declare4Py.ProcessModels.DeclareModel import DeclareModelTemplate"
   ],
   "outputs": [],
   "execution_count": 8
  },
  {
   "cell_type": "markdown",
   "id": "0eb4454a",
   "metadata": {},
   "source": [
    "The DECLARE constraints supported by Declare4Py can be retrieved with the `get_unary_templates()` and `get_binary_templates` methods of the `DeclareModelTemplate` class:"
   ]
  },
  {
   "cell_type": "code",
   "id": "def7e392",
   "metadata": {
    "ExecuteTime": {
     "end_time": "2026-05-29T13:48:54.092077400Z",
     "start_time": "2026-05-29T13:48:54.057153200Z"
    }
   },
   "source": [
    "unary_templates = DeclareModelTemplate.get_unary_templates()\n",
    "binary_templates = DeclareModelTemplate.get_binary_templates()\n",
    "\n",
    "print(\"Unary templates:\")\n",
    "print(\"-----------------\")\n",
    "for template in unary_templates:\n",
    "    print(template.templ_str)\n",
    "print(\"\\n\")\n",
    "\n",
    "print(\"Binary templates:\")\n",
    "print(\"-----------------\")\n",
    "for template in binary_templates:\n",
    "    print(template.templ_str)"
   ],
   "outputs": [
    {
     "name": "stdout",
     "output_type": "stream",
     "text": [
      "Unary templates:\n",
      "-----------------\n",
      "Existence\n",
      "Absence\n",
      "Exactly\n",
      "Init\n",
      "End\n",
      "\n",
      "\n",
      "Binary templates:\n",
      "-----------------\n",
      "Choice\n",
      "Exclusive Choice\n",
      "Responded Existence\n",
      "Response\n",
      "Alternate Response\n",
      "Chain Response\n",
      "Precedence\n",
      "Alternate Precedence\n",
      "Chain Precedence\n",
      "Succession\n",
      "Alternate Succession\n",
      "Co-Existence\n",
      "Chain Succession\n",
      "Not Chain Succession\n",
      "Not Co-Existence\n",
      "Not Succession\n",
      "Not Responded Existence\n",
      "Not Response\n",
      "Not Precedence\n",
      "Not Chain Response\n",
      "Not Chain Precedence\n"
     ]
    }
   ],
   "execution_count": 9
  },
  {
   "cell_type": "markdown",
   "id": "d91ab132",
   "metadata": {},
   "source": [
    "Notice that for the templates `Existence`, `Absence` and `Exactly` an additional parameter is necessary for the cardinality. This has to be encoded in the DECLARE `.decl` model with a numeric suffix, for example `Exactly2` or `Existence23`.\n",
    "\n",
    "The next step is the parsing a DECLARE model."
   ]
  },
  {
   "cell_type": "code",
   "id": "3c01ba4c",
   "metadata": {
    "ExecuteTime": {
     "end_time": "2026-05-29T13:48:54.121552300Z",
     "start_time": "2026-05-29T13:48:54.094147300Z"
    }
   },
   "source": [
    "model_path = os.path.join(\"../../../\", \"tests\", \"test_models\",\"data_model.decl\")\n",
    "declare_model = DeclareModel().parse_from_file(model_path)"
   ],
   "outputs": [],
   "execution_count": 10
  },
  {
   "cell_type": "markdown",
   "id": "78887621",
   "metadata": {},
   "source": [
    "The DECLARE model can be inspected by getting all the activity names or the constraints. This information is returned as a list of strings."
   ]
  },
  {
   "cell_type": "code",
   "id": "682d8841",
   "metadata": {
    "ExecuteTime": {
     "end_time": "2026-05-29T13:49:05.172376500Z",
     "start_time": "2026-05-29T13:49:05.145375600Z"
    }
   },
   "source": [
    "model_activities = declare_model.get_decl_model_activities()\n",
    "model_constraints = declare_model.get_decl_model_constraints()\n",
    "\n",
    "print(\"Model activities:\")\n",
    "print(\"-----------------\")\n",
    "for idx, act in enumerate(model_activities):\n",
    "    print(idx, act)\n",
    "print(\"\\n\")\n",
    "\n",
    "print(\"Model constraints:\")\n",
    "print(\"-----------------\")\n",
    "for idx, constr in enumerate(model_constraints):\n",
    "    print(idx, constr)"
   ],
   "outputs": [
    {
     "name": "stdout",
     "output_type": "stream",
     "text": [
      "Model activities:\n",
      "-----------------\n",
      "0 ER Triage\n",
      "1 ER Registration\n",
      "2 ER Sepsis Triage\n",
      "3 Leucocytes\n",
      "4 CRP\n",
      "5 LacticAcid\n",
      "6 IV Antibiotics\n",
      "7 Admission NC\n",
      "8 IV Liquid\n",
      "9 Release A\n",
      "10 Return ER\n",
      "11 Admission IC\n",
      "\n",
      "\n",
      "Model constraints:\n",
      "-----------------\n",
      "0 Existence2[Admission NC] | |\n",
      "1 Chain Response[Admission NC, Release B] |A.org:group is K |T.org:group is E |\n",
      "2 Chain Response[Admission NC, Release A] |A.org:group is I |T.org:group is E |133020,957701,s\n",
      "3 Chain Precedence[IV Liquid, Admission NC] |A.org:group is I |T.org:group is A |92,14473,s\n",
      "4 Chain Response[ER Registration, ER Triage] |(A.DiagnosticArtAstrup is false) AND (A.SIRSCritHeartRate is true) AND (A.org:group is A) AND (A.DiagnosticBlood is true) AND (A.DisfuncOrg is false) AND (A.DiagnosticECG is true) AND (A.Age >= 45) AND (A.InfectionSuspected is true) AND (A.DiagnosticLacticAcid is true) AND (A.DiagnosticSputum is true) AND (A.Hypoxie is false) AND (A.DiagnosticUrinaryCulture is true) AND (A.DiagnosticLiquor is false) AND (A.SIRSCritTemperature is true) AND (A.Infusion is true) AND (A.Hypotensie is false) AND (A.DiagnosticUrinarySediment is true) AND (A.Oligurie is false) AND (A.Age <= 80) AND (A.SIRSCritTachypnea is true) AND (A.DiagnosticOther is false) AND (A.SIRSCritLeucos is false) AND (A.DiagnosticIC is true) AND (A.SIRSCriteria2OrMore is true) AND (A.DiagnosticXthorax is true) |T.org:group is C |52,2154,s\n",
      "5 Chain Precedence[Release A, Return ER] |A.org:group is ? |T.org:group is E |1121801,1121801,s\n",
      "6 Chain Precedence[ER Sepsis Triage, IV Antibiotics] |A.org:group is L |T.org:group is L |15,11000,s\n",
      "7 Chain Response[ER Sepsis Triage, IV Antibiotics] |A.org:group is L |T.org:group is L |15,11000,s\n",
      "8 Chain Precedence[Admission IC, Admission NC] |A.org:group is J |T.org:group is J |\n",
      "9 Chain Precedence[IV Antibiotics, Admission NC] |A.org:group is F |T.org:group is A |92,14459,s\n",
      "10 Chain Precedence[Admission NC, Release B] |A.org:group is E |T.org:group is K |48225,48225,s\n",
      "11 Chain Response[Admission IC, Admission NC] |A.org:group is J |T.org:group is J |61534,61534,s\n",
      "12 Chain Response[LacticAcid, Leucocytes] |A.LacticAcid <= 0.8 |T.Leucocytes >= 13.8 |0,2778,m\n",
      "13 Chain Precedence[ER Registration, ER Triage] |A.org:group is C |(T.InfectionSuspected is true) AND (T.SIRSCritTemperature is true) AND (T.DiagnosticLacticAcid is true) AND (T.DiagnosticBlood is true) AND (T.DiagnosticIC is true) AND (T.SIRSCriteria2OrMore is true) AND (T.DiagnosticECG is true) |52,2154,s\n"
     ]
    }
   ],
   "execution_count": 12
  }
 ],
 "metadata": {
  "kernelspec": {
   "display_name": "Python 3 (ipykernel)",
   "language": "python",
   "name": "python3"
  },
  "language_info": {
   "codemirror_mode": {
    "name": "ipython",
    "version": 3
   },
   "file_extension": ".py",
   "mimetype": "text/x-python",
   "name": "python",
   "nbconvert_exporter": "python",
   "pygments_lexer": "ipython3",
   "version": "3.11.4"
  },
  "vscode": {
   "interpreter": {
    "hash": "05d4b7c3cd0aad81aa9df4db91d3eeeb2841d831664bc3cb6ce2ef5b755f059a"
   }
  }
 },
 "nbformat": 4,
 "nbformat_minor": 5
}