{
 "cells": [
  {
   "metadata": {
    "ExecuteTime": {
     "end_time": "2026-05-29T13:59:52.391046600Z",
     "start_time": "2026-05-29T13:59:52.353537Z"
    }
   },
   "cell_type": "code",
   "source": [
    "import warnings\n",
    "warnings.filterwarnings(\"ignore\", category=UserWarning)"
   ],
   "outputs": [],
   "execution_count": 1
  },
  {
   "cell_type": "markdown",
   "metadata": {},
   "source": [
    "# Conformance Checking with a LTLf model\n",
    "\n",
    "The class `ProcessMiningTasks.ConformanceChecking.LTLAnalyzer.LTLAnalyzer` provides a way to check if the log conforms to a Linear Temporal Logic on finite traces (LTLf) formula. The formula can be a provided by the user as a string, note that we adopted the LTLf syntax [here](http://ltlf2dfa.diag.uniroma1.it/ltlf_syntax). In addition, we also provide the following set of LTLf templates:\n",
    "\n",
    "1. `eventually_a`;\n",
    "2. `next_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",
    "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",
    "First of all, an event log has to be imported."
   ]
  },
  {
   "cell_type": "code",
   "metadata": {
    "ExecuteTime": {
     "end_time": "2026-05-29T13:59:55.623950400Z",
     "start_time": "2026-05-29T13:59:52.812774500Z"
    }
   },
   "source": [
    "import os\n",
    "from Declare4Py.D4PyEventLog import D4PyEventLog\n",
    "\n",
    "log_path = os.path.join(\"../../../\", \"tests\", \"test_logs\",\"Sepsis Cases.xes.gz\")\n",
    "event_log = D4PyEventLog()\n",
    "event_log.parse_xes_log(log_path)"
   ],
   "outputs": [
    {
     "data": {
      "text/plain": [
       "parsing log, completed traces ::   0%|          | 0/1050 [00:00<?, ?it/s]"
      ],
      "application/vnd.jupyter.widget-view+json": {
       "version_major": 2,
       "version_minor": 0,
       "model_id": "5d63a04e639e459d84fc600d237b7132"
      }
     },
     "metadata": {},
     "output_type": "display_data"
    }
   ],
   "execution_count": 2
  },
  {
   "cell_type": "markdown",
   "metadata": {},
   "source": [
    "The next step is to create an `LTLModel` from an input LTLf formula in string format with the class `ProcessModels.LTLModel.LTLModel` and pass it to the LTL conformance checker implemented in the `src.Declare4Py.ProcessMiningTasks.ConformanceChecking.LTLAnalyzer.LTLAnalyzer` class. The corresponding method `run` will do the conformance checking and return a Pandas dataframe. This dataframe contains the traces ids in the first column and the results of the conformance checking in the second column. The `run` method transforms the LTLf formula into a Deterministic Finite state Automaton (DFA) and checks whether a trace in a log is accepted. 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",
    "As explained in the tutorial regarding process models, it is possible to switch the backends of the LTLf model with the `to_ltlf2dfa_backend` and `to_lydia_backend` methods. The default backend is Lydia.\n",
    "\n",
    "For speeding up the computation, the `run` method takes as input the integer parameter `jobs` that sets the number of processes to run in parallel. Each process considers a portion of the input event log. The default value of the number of jobs is 1. Note that, with small logs (i.e., with a small number of events) the performance with multiple jobs can be comparable with the ones of a single job.\n",
    "\n",
    "We show an example of LTLf conformance checking with the `F(ER Triage)` formula."
   ]
  },
  {
   "cell_type": "code",
   "metadata": {
    "ExecuteTime": {
     "end_time": "2026-05-29T13:59:58.348521500Z",
     "start_time": "2026-05-29T13:59:55.629950200Z"
    }
   },
   "source": [
    "from Declare4Py.ProcessModels.LTLModel import LTLModel\n",
    "from Declare4Py.ProcessMiningTasks.ConformanceChecking.LTLAnalyzer import LTLAnalyzer\n",
    "\n",
    "model = LTLModel()\n",
    "model.parse_from_string(\"F(CRP)\")\n",
    "\n",
    "analyzer = LTLAnalyzer(event_log, model)\n",
    "conf_check_res_df = analyzer.run(jobs=2)\n",
    "conf_check_res_df"
   ],
   "outputs": [
    {
     "data": {
      "text/plain": [
       "     case:concept:name  accepted\n",
       "0                    A     False\n",
       "1                    B     False\n",
       "2                    C     False\n",
       "3                    D     False\n",
       "4                    E     False\n",
       "...                ...       ...\n",
       "1045               HNA     False\n",
       "1046               INA     False\n",
       "1047               JNA     False\n",
       "1048               KNA     False\n",
       "1049               LNA     False\n",
       "\n",
       "[1050 rows x 2 columns]"
      ],
      "text/html": [
       "<div>\n",
       "<style scoped>\n",
       "    .dataframe tbody tr th:only-of-type {\n",
       "        vertical-align: middle;\n",
       "    }\n",
       "\n",
       "    .dataframe tbody tr th {\n",
       "        vertical-align: top;\n",
       "    }\n",
       "\n",
       "    .dataframe thead th {\n",
       "        text-align: right;\n",
       "    }\n",
       "</style>\n",
       "<table border=\"1\" class=\"dataframe\">\n",
       "  <thead>\n",
       "    <tr style=\"text-align: right;\">\n",
       "      <th></th>\n",
       "      <th>case:concept:name</th>\n",
       "      <th>accepted</th>\n",
       "    </tr>\n",
       "  </thead>\n",
       "  <tbody>\n",
       "    <tr>\n",
       "      <th>0</th>\n",
       "      <td>A</td>\n",
       "      <td>False</td>\n",
       "    </tr>\n",
       "    <tr>\n",
       "      <th>1</th>\n",
       "      <td>B</td>\n",
       "      <td>False</td>\n",
       "    </tr>\n",
       "    <tr>\n",
       "      <th>2</th>\n",
       "      <td>C</td>\n",
       "      <td>False</td>\n",
       "    </tr>\n",
       "    <tr>\n",
       "      <th>3</th>\n",
       "      <td>D</td>\n",
       "      <td>False</td>\n",
       "    </tr>\n",
       "    <tr>\n",
       "      <th>4</th>\n",
       "      <td>E</td>\n",
       "      <td>False</td>\n",
       "    </tr>\n",
       "    <tr>\n",
       "      <th>...</th>\n",
       "      <td>...</td>\n",
       "      <td>...</td>\n",
       "    </tr>\n",
       "    <tr>\n",
       "      <th>1045</th>\n",
       "      <td>HNA</td>\n",
       "      <td>False</td>\n",
       "    </tr>\n",
       "    <tr>\n",
       "      <th>1046</th>\n",
       "      <td>INA</td>\n",
       "      <td>False</td>\n",
       "    </tr>\n",
       "    <tr>\n",
       "      <th>1047</th>\n",
       "      <td>JNA</td>\n",
       "      <td>False</td>\n",
       "    </tr>\n",
       "    <tr>\n",
       "      <th>1048</th>\n",
       "      <td>KNA</td>\n",
       "      <td>False</td>\n",
       "    </tr>\n",
       "    <tr>\n",
       "      <th>1049</th>\n",
       "      <td>LNA</td>\n",
       "      <td>False</td>\n",
       "    </tr>\n",
       "  </tbody>\n",
       "</table>\n",
       "<p>1050 rows × 2 columns</p>\n",
       "</div>"
      ]
     },
     "execution_count": 3,
     "metadata": {},
     "output_type": "execute_result"
    }
   ],
   "execution_count": 3
  },
  {
   "cell_type": "markdown",
   "metadata": {},
   "source": [
    "## Conformance Checking with LTLf Templates\n",
    "\n",
    "Declare4Py offers some LTLf templates in the `src.Declare4Py.ProcessModels.LTLModel.LTLTemplate` class. You just need to instantiate a single template by passing the template name to the `LTLTemplate` class and then filling the template with some proper activities to obtain an `LTLModel` and run the LTL checker.\n",
    "\n",
    "The `LTLTemplate`'s function `fill_template` expects a list with the parameters equal to those expected by the template and a list of attribute types and returns an `LTLModel` object containing the parsed formula of the template and the list of attribute types. The LTLf formula of the template can be retrieved by accessing the `formula` attribute of the `LTLModel` object.\n",
    "\n",
    "### `eventually_a`\n",
    "\n",
    "This is a unary template taking one activity as input. The corresponding LTLf formula is `F(a)`."
   ]
  },
  {
   "cell_type": "code",
   "metadata": {
    "ExecuteTime": {
     "end_time": "2026-05-29T13:59:59.145238900Z",
     "start_time": "2026-05-29T13:59:58.433335500Z"
    }
   },
   "source": [
    "from Declare4Py.ProcessModels.LTLModel import LTLTemplate\n",
    "\n",
    "template: LTLTemplate = LTLTemplate('eventually_a')\n",
    "model: LTLModel = template.fill_template(['CRP'])\n",
    "print(f\"Formula: {model.formula}\")\n",
    "analyzer = LTLAnalyzer(event_log, model)\n",
    "conf_check_res_df = analyzer.run()\n",
    "conf_check_res_df"
   ],
   "outputs": [
    {
     "name": "stdout",
     "output_type": "stream",
     "text": [
      "Formula: F(con_crp)\n"
     ]
    },
    {
     "data": {
      "text/plain": [
       "     case:concept:name  accepted\n",
       "0                    A      True\n",
       "1                    B      True\n",
       "2                    C      True\n",
       "3                    D      True\n",
       "4                    E      True\n",
       "...                ...       ...\n",
       "1045               HNA      True\n",
       "1046               INA     False\n",
       "1047               JNA     False\n",
       "1048               KNA      True\n",
       "1049               LNA     False\n",
       "\n",
       "[1050 rows x 2 columns]"
      ],
      "text/html": [
       "<div>\n",
       "<style scoped>\n",
       "    .dataframe tbody tr th:only-of-type {\n",
       "        vertical-align: middle;\n",
       "    }\n",
       "\n",
       "    .dataframe tbody tr th {\n",
       "        vertical-align: top;\n",
       "    }\n",
       "\n",
       "    .dataframe thead th {\n",
       "        text-align: right;\n",
       "    }\n",
       "</style>\n",
       "<table border=\"1\" class=\"dataframe\">\n",
       "  <thead>\n",
       "    <tr style=\"text-align: right;\">\n",
       "      <th></th>\n",
       "      <th>case:concept:name</th>\n",
       "      <th>accepted</th>\n",
       "    </tr>\n",
       "  </thead>\n",
       "  <tbody>\n",
       "    <tr>\n",
       "      <th>0</th>\n",
       "      <td>A</td>\n",
       "      <td>True</td>\n",
       "    </tr>\n",
       "    <tr>\n",
       "      <th>1</th>\n",
       "      <td>B</td>\n",
       "      <td>True</td>\n",
       "    </tr>\n",
       "    <tr>\n",
       "      <th>2</th>\n",
       "      <td>C</td>\n",
       "      <td>True</td>\n",
       "    </tr>\n",
       "    <tr>\n",
       "      <th>3</th>\n",
       "      <td>D</td>\n",
       "      <td>True</td>\n",
       "    </tr>\n",
       "    <tr>\n",
       "      <th>4</th>\n",
       "      <td>E</td>\n",
       "      <td>True</td>\n",
       "    </tr>\n",
       "    <tr>\n",
       "      <th>...</th>\n",
       "      <td>...</td>\n",
       "      <td>...</td>\n",
       "    </tr>\n",
       "    <tr>\n",
       "      <th>1045</th>\n",
       "      <td>HNA</td>\n",
       "      <td>True</td>\n",
       "    </tr>\n",
       "    <tr>\n",
       "      <th>1046</th>\n",
       "      <td>INA</td>\n",
       "      <td>False</td>\n",
       "    </tr>\n",
       "    <tr>\n",
       "      <th>1047</th>\n",
       "      <td>JNA</td>\n",
       "      <td>False</td>\n",
       "    </tr>\n",
       "    <tr>\n",
       "      <th>1048</th>\n",
       "      <td>KNA</td>\n",
       "      <td>True</td>\n",
       "    </tr>\n",
       "    <tr>\n",
       "      <th>1049</th>\n",
       "      <td>LNA</td>\n",
       "      <td>False</td>\n",
       "    </tr>\n",
       "  </tbody>\n",
       "</table>\n",
       "<p>1050 rows × 2 columns</p>\n",
       "</div>"
      ]
     },
     "execution_count": 4,
     "metadata": {},
     "output_type": "execute_result"
    }
   ],
   "execution_count": 4
  },
  {
   "cell_type": "markdown",
   "metadata": {},
   "source": [
    "### `next_a`\n",
    "This is a unary template taking one activity as input. The corresponding LTLf formula is `X(a)`."
   ]
  },
  {
   "cell_type": "code",
   "metadata": {
    "scrolled": true,
    "ExecuteTime": {
     "end_time": "2026-05-29T14:00:00.773745100Z",
     "start_time": "2026-05-29T14:00:00.182943200Z"
    }
   },
   "source": [
    "template = LTLTemplate('next_a')\n",
    "model = template.fill_template(['ER Triage'])\n",
    "print(f\"Formula: {model.formula}\")\n",
    "analyzer = LTLAnalyzer(event_log, model)\n",
    "conf_check_res_df = analyzer.run()\n",
    "conf_check_res_df"
   ],
   "outputs": [
    {
     "name": "stdout",
     "output_type": "stream",
     "text": [
      "Formula: X[!](con_ertriage)\n"
     ]
    },
    {
     "data": {
      "text/plain": [
       "     case:concept:name  accepted\n",
       "0                    A     False\n",
       "1                    B      True\n",
       "2                    C      True\n",
       "3                    D      True\n",
       "4                    E      True\n",
       "...                ...       ...\n",
       "1045               HNA      True\n",
       "1046               INA      True\n",
       "1047               JNA      True\n",
       "1048               KNA      True\n",
       "1049               LNA      True\n",
       "\n",
       "[1050 rows x 2 columns]"
      ],
      "text/html": [
       "<div>\n",
       "<style scoped>\n",
       "    .dataframe tbody tr th:only-of-type {\n",
       "        vertical-align: middle;\n",
       "    }\n",
       "\n",
       "    .dataframe tbody tr th {\n",
       "        vertical-align: top;\n",
       "    }\n",
       "\n",
       "    .dataframe thead th {\n",
       "        text-align: right;\n",
       "    }\n",
       "</style>\n",
       "<table border=\"1\" class=\"dataframe\">\n",
       "  <thead>\n",
       "    <tr style=\"text-align: right;\">\n",
       "      <th></th>\n",
       "      <th>case:concept:name</th>\n",
       "      <th>accepted</th>\n",
       "    </tr>\n",
       "  </thead>\n",
       "  <tbody>\n",
       "    <tr>\n",
       "      <th>0</th>\n",
       "      <td>A</td>\n",
       "      <td>False</td>\n",
       "    </tr>\n",
       "    <tr>\n",
       "      <th>1</th>\n",
       "      <td>B</td>\n",
       "      <td>True</td>\n",
       "    </tr>\n",
       "    <tr>\n",
       "      <th>2</th>\n",
       "      <td>C</td>\n",
       "      <td>True</td>\n",
       "    </tr>\n",
       "    <tr>\n",
       "      <th>3</th>\n",
       "      <td>D</td>\n",
       "      <td>True</td>\n",
       "    </tr>\n",
       "    <tr>\n",
       "      <th>4</th>\n",
       "      <td>E</td>\n",
       "      <td>True</td>\n",
       "    </tr>\n",
       "    <tr>\n",
       "      <th>...</th>\n",
       "      <td>...</td>\n",
       "      <td>...</td>\n",
       "    </tr>\n",
       "    <tr>\n",
       "      <th>1045</th>\n",
       "      <td>HNA</td>\n",
       "      <td>True</td>\n",
       "    </tr>\n",
       "    <tr>\n",
       "      <th>1046</th>\n",
       "      <td>INA</td>\n",
       "      <td>True</td>\n",
       "    </tr>\n",
       "    <tr>\n",
       "      <th>1047</th>\n",
       "      <td>JNA</td>\n",
       "      <td>True</td>\n",
       "    </tr>\n",
       "    <tr>\n",
       "      <th>1048</th>\n",
       "      <td>KNA</td>\n",
       "      <td>True</td>\n",
       "    </tr>\n",
       "    <tr>\n",
       "      <th>1049</th>\n",
       "      <td>LNA</td>\n",
       "      <td>True</td>\n",
       "    </tr>\n",
       "  </tbody>\n",
       "</table>\n",
       "<p>1050 rows × 2 columns</p>\n",
       "</div>"
      ]
     },
     "execution_count": 5,
     "metadata": {},
     "output_type": "execute_result"
    }
   ],
   "execution_count": 5
  },
  {
   "cell_type": "markdown",
   "metadata": {},
   "source": [
    "### `eventually_a_and_eventually_b`\n",
    "This is a binary template taking two activities as input. The corresponding LTLf formula is `F(a) && F(b)`."
   ]
  },
  {
   "cell_type": "code",
   "metadata": {
    "ExecuteTime": {
     "end_time": "2026-05-29T14:00:02.230595600Z",
     "start_time": "2026-05-29T14:00:00.843306200Z"
    }
   },
   "source": [
    "template = LTLTemplate('eventually_a_and_eventually_b')\n",
    "model = template.fill_template(['Leucocytes', 'CRP'])\n",
    "print(f\"Formula: {model.formula}\")\n",
    "analyzer = LTLAnalyzer(event_log, model)\n",
    "conf_check_res_df = analyzer.run()\n",
    "conf_check_res_df"
   ],
   "outputs": [
    {
     "name": "stdout",
     "output_type": "stream",
     "text": [
      "Formula: F(con_leucocytes)  && F(con_crp)\n"
     ]
    },
    {
     "data": {
      "text/plain": [
       "     case:concept:name  accepted\n",
       "0                    A      True\n",
       "1                    B      True\n",
       "2                    C      True\n",
       "3                    D      True\n",
       "4                    E      True\n",
       "...                ...       ...\n",
       "1045               HNA      True\n",
       "1046               INA     False\n",
       "1047               JNA     False\n",
       "1048               KNA      True\n",
       "1049               LNA     False\n",
       "\n",
       "[1050 rows x 2 columns]"
      ],
      "text/html": [
       "<div>\n",
       "<style scoped>\n",
       "    .dataframe tbody tr th:only-of-type {\n",
       "        vertical-align: middle;\n",
       "    }\n",
       "\n",
       "    .dataframe tbody tr th {\n",
       "        vertical-align: top;\n",
       "    }\n",
       "\n",
       "    .dataframe thead th {\n",
       "        text-align: right;\n",
       "    }\n",
       "</style>\n",
       "<table border=\"1\" class=\"dataframe\">\n",
       "  <thead>\n",
       "    <tr style=\"text-align: right;\">\n",
       "      <th></th>\n",
       "      <th>case:concept:name</th>\n",
       "      <th>accepted</th>\n",
       "    </tr>\n",
       "  </thead>\n",
       "  <tbody>\n",
       "    <tr>\n",
       "      <th>0</th>\n",
       "      <td>A</td>\n",
       "      <td>True</td>\n",
       "    </tr>\n",
       "    <tr>\n",
       "      <th>1</th>\n",
       "      <td>B</td>\n",
       "      <td>True</td>\n",
       "    </tr>\n",
       "    <tr>\n",
       "      <th>2</th>\n",
       "      <td>C</td>\n",
       "      <td>True</td>\n",
       "    </tr>\n",
       "    <tr>\n",
       "      <th>3</th>\n",
       "      <td>D</td>\n",
       "      <td>True</td>\n",
       "    </tr>\n",
       "    <tr>\n",
       "      <th>4</th>\n",
       "      <td>E</td>\n",
       "      <td>True</td>\n",
       "    </tr>\n",
       "    <tr>\n",
       "      <th>...</th>\n",
       "      <td>...</td>\n",
       "      <td>...</td>\n",
       "    </tr>\n",
       "    <tr>\n",
       "      <th>1045</th>\n",
       "      <td>HNA</td>\n",
       "      <td>True</td>\n",
       "    </tr>\n",
       "    <tr>\n",
       "      <th>1046</th>\n",
       "      <td>INA</td>\n",
       "      <td>False</td>\n",
       "    </tr>\n",
       "    <tr>\n",
       "      <th>1047</th>\n",
       "      <td>JNA</td>\n",
       "      <td>False</td>\n",
       "    </tr>\n",
       "    <tr>\n",
       "      <th>1048</th>\n",
       "      <td>KNA</td>\n",
       "      <td>True</td>\n",
       "    </tr>\n",
       "    <tr>\n",
       "      <th>1049</th>\n",
       "      <td>LNA</td>\n",
       "      <td>False</td>\n",
       "    </tr>\n",
       "  </tbody>\n",
       "</table>\n",
       "<p>1050 rows × 2 columns</p>\n",
       "</div>"
      ]
     },
     "execution_count": 6,
     "metadata": {},
     "output_type": "execute_result"
    }
   ],
   "execution_count": 6
  },
  {
   "cell_type": "markdown",
   "metadata": {},
   "source": [
    "### `eventually_a_then_b`\n",
    "\n",
    "This is a binary template taking two activities as input. The corresponding LTLf formula is `F(a && F(b))`."
   ]
  },
  {
   "cell_type": "code",
   "metadata": {
    "ExecuteTime": {
     "end_time": "2026-05-29T14:00:04.414188900Z",
     "start_time": "2026-05-29T14:00:03.276086700Z"
    }
   },
   "source": [
    "template = LTLTemplate('eventually_a_then_b')\n",
    "model = template.fill_template(['Leucocytes', 'CRP'])\n",
    "print(f\"Formula: {model.formula}\")\n",
    "analyzer = LTLAnalyzer(event_log, model)\n",
    "conf_check_res_df = analyzer.run()\n",
    "conf_check_res_df"
   ],
   "outputs": [
    {
     "name": "stdout",
     "output_type": "stream",
     "text": [
      "Formula: F(con_leucocytes  && F(con_crp))\n"
     ]
    },
    {
     "data": {
      "text/plain": [
       "     case:concept:name  accepted\n",
       "0                    A      True\n",
       "1                    B      True\n",
       "2                    C      True\n",
       "3                    D      True\n",
       "4                    E     False\n",
       "...                ...       ...\n",
       "1045               HNA      True\n",
       "1046               INA     False\n",
       "1047               JNA     False\n",
       "1048               KNA      True\n",
       "1049               LNA     False\n",
       "\n",
       "[1050 rows x 2 columns]"
      ],
      "text/html": [
       "<div>\n",
       "<style scoped>\n",
       "    .dataframe tbody tr th:only-of-type {\n",
       "        vertical-align: middle;\n",
       "    }\n",
       "\n",
       "    .dataframe tbody tr th {\n",
       "        vertical-align: top;\n",
       "    }\n",
       "\n",
       "    .dataframe thead th {\n",
       "        text-align: right;\n",
       "    }\n",
       "</style>\n",
       "<table border=\"1\" class=\"dataframe\">\n",
       "  <thead>\n",
       "    <tr style=\"text-align: right;\">\n",
       "      <th></th>\n",
       "      <th>case:concept:name</th>\n",
       "      <th>accepted</th>\n",
       "    </tr>\n",
       "  </thead>\n",
       "  <tbody>\n",
       "    <tr>\n",
       "      <th>0</th>\n",
       "      <td>A</td>\n",
       "      <td>True</td>\n",
       "    </tr>\n",
       "    <tr>\n",
       "      <th>1</th>\n",
       "      <td>B</td>\n",
       "      <td>True</td>\n",
       "    </tr>\n",
       "    <tr>\n",
       "      <th>2</th>\n",
       "      <td>C</td>\n",
       "      <td>True</td>\n",
       "    </tr>\n",
       "    <tr>\n",
       "      <th>3</th>\n",
       "      <td>D</td>\n",
       "      <td>True</td>\n",
       "    </tr>\n",
       "    <tr>\n",
       "      <th>4</th>\n",
       "      <td>E</td>\n",
       "      <td>False</td>\n",
       "    </tr>\n",
       "    <tr>\n",
       "      <th>...</th>\n",
       "      <td>...</td>\n",
       "      <td>...</td>\n",
       "    </tr>\n",
       "    <tr>\n",
       "      <th>1045</th>\n",
       "      <td>HNA</td>\n",
       "      <td>True</td>\n",
       "    </tr>\n",
       "    <tr>\n",
       "      <th>1046</th>\n",
       "      <td>INA</td>\n",
       "      <td>False</td>\n",
       "    </tr>\n",
       "    <tr>\n",
       "      <th>1047</th>\n",
       "      <td>JNA</td>\n",
       "      <td>False</td>\n",
       "    </tr>\n",
       "    <tr>\n",
       "      <th>1048</th>\n",
       "      <td>KNA</td>\n",
       "      <td>True</td>\n",
       "    </tr>\n",
       "    <tr>\n",
       "      <th>1049</th>\n",
       "      <td>LNA</td>\n",
       "      <td>False</td>\n",
       "    </tr>\n",
       "  </tbody>\n",
       "</table>\n",
       "<p>1050 rows × 2 columns</p>\n",
       "</div>"
      ]
     },
     "execution_count": 7,
     "metadata": {},
     "output_type": "execute_result"
    }
   ],
   "execution_count": 7
  },
  {
   "cell_type": "markdown",
   "metadata": {},
   "source": [
    "### `eventually_a_or_b`\n",
    "\n",
    "This is a binary template taking two activities as input. The corresponding LTLf formula is `F(a) || F(b)`."
   ]
  },
  {
   "cell_type": "code",
   "metadata": {
    "ExecuteTime": {
     "end_time": "2026-05-29T14:00:05.378166800Z",
     "start_time": "2026-05-29T14:00:04.469606Z"
    }
   },
   "source": [
    "template = LTLTemplate('eventually_a_or_b')\n",
    "model = template.fill_template(['Leucocytes', 'CRP'])\n",
    "print(f\"Formula: {model.formula}\")\n",
    "analyzer = LTLAnalyzer(event_log, model)\n",
    "conf_check_res_df = analyzer.run()\n",
    "conf_check_res_df"
   ],
   "outputs": [
    {
     "name": "stdout",
     "output_type": "stream",
     "text": [
      "Formula: F(con_leucocytes) || F(con_crp)\n"
     ]
    },
    {
     "data": {
      "text/plain": [
       "     case:concept:name  accepted\n",
       "0                    A      True\n",
       "1                    B      True\n",
       "2                    C      True\n",
       "3                    D      True\n",
       "4                    E      True\n",
       "...                ...       ...\n",
       "1045               HNA      True\n",
       "1046               INA     False\n",
       "1047               JNA     False\n",
       "1048               KNA      True\n",
       "1049               LNA     False\n",
       "\n",
       "[1050 rows x 2 columns]"
      ],
      "text/html": [
       "<div>\n",
       "<style scoped>\n",
       "    .dataframe tbody tr th:only-of-type {\n",
       "        vertical-align: middle;\n",
       "    }\n",
       "\n",
       "    .dataframe tbody tr th {\n",
       "        vertical-align: top;\n",
       "    }\n",
       "\n",
       "    .dataframe thead th {\n",
       "        text-align: right;\n",
       "    }\n",
       "</style>\n",
       "<table border=\"1\" class=\"dataframe\">\n",
       "  <thead>\n",
       "    <tr style=\"text-align: right;\">\n",
       "      <th></th>\n",
       "      <th>case:concept:name</th>\n",
       "      <th>accepted</th>\n",
       "    </tr>\n",
       "  </thead>\n",
       "  <tbody>\n",
       "    <tr>\n",
       "      <th>0</th>\n",
       "      <td>A</td>\n",
       "      <td>True</td>\n",
       "    </tr>\n",
       "    <tr>\n",
       "      <th>1</th>\n",
       "      <td>B</td>\n",
       "      <td>True</td>\n",
       "    </tr>\n",
       "    <tr>\n",
       "      <th>2</th>\n",
       "      <td>C</td>\n",
       "      <td>True</td>\n",
       "    </tr>\n",
       "    <tr>\n",
       "      <th>3</th>\n",
       "      <td>D</td>\n",
       "      <td>True</td>\n",
       "    </tr>\n",
       "    <tr>\n",
       "      <th>4</th>\n",
       "      <td>E</td>\n",
       "      <td>True</td>\n",
       "    </tr>\n",
       "    <tr>\n",
       "      <th>...</th>\n",
       "      <td>...</td>\n",
       "      <td>...</td>\n",
       "    </tr>\n",
       "    <tr>\n",
       "      <th>1045</th>\n",
       "      <td>HNA</td>\n",
       "      <td>True</td>\n",
       "    </tr>\n",
       "    <tr>\n",
       "      <th>1046</th>\n",
       "      <td>INA</td>\n",
       "      <td>False</td>\n",
       "    </tr>\n",
       "    <tr>\n",
       "      <th>1047</th>\n",
       "      <td>JNA</td>\n",
       "      <td>False</td>\n",
       "    </tr>\n",
       "    <tr>\n",
       "      <th>1048</th>\n",
       "      <td>KNA</td>\n",
       "      <td>True</td>\n",
       "    </tr>\n",
       "    <tr>\n",
       "      <th>1049</th>\n",
       "      <td>LNA</td>\n",
       "      <td>False</td>\n",
       "    </tr>\n",
       "  </tbody>\n",
       "</table>\n",
       "<p>1050 rows × 2 columns</p>\n",
       "</div>"
      ]
     },
     "execution_count": 8,
     "metadata": {},
     "output_type": "execute_result"
    }
   ],
   "execution_count": 8
  },
  {
   "cell_type": "markdown",
   "metadata": {},
   "source": [
    "### `eventually_a_next_b`\n",
    "\n",
    "This is a binary template taking two activities as input. The corresponding LTLf formula is `F(a && X(b))`."
   ]
  },
  {
   "cell_type": "code",
   "metadata": {
    "ExecuteTime": {
     "end_time": "2026-05-29T14:00:07.391075800Z",
     "start_time": "2026-05-29T14:00:06.408564300Z"
    }
   },
   "source": [
    "template = LTLTemplate('eventually_a_next_b')\n",
    "model = template.fill_template(['Leucocytes', 'CRP'])\n",
    "print(f\"Formula: {model.formula}\")\n",
    "analyzer = LTLAnalyzer(event_log, model)\n",
    "conf_check_res_df = analyzer.run()\n",
    "conf_check_res_df"
   ],
   "outputs": [
    {
     "name": "stdout",
     "output_type": "stream",
     "text": [
      "Formula: F(con_leucocytes  && X[!](con_crp))\n"
     ]
    },
    {
     "data": {
      "text/plain": [
       "     case:concept:name  accepted\n",
       "0                    A      True\n",
       "1                    B     False\n",
       "2                    C      True\n",
       "3                    D      True\n",
       "4                    E     False\n",
       "...                ...       ...\n",
       "1045               HNA      True\n",
       "1046               INA     False\n",
       "1047               JNA     False\n",
       "1048               KNA      True\n",
       "1049               LNA     False\n",
       "\n",
       "[1050 rows x 2 columns]"
      ],
      "text/html": [
       "<div>\n",
       "<style scoped>\n",
       "    .dataframe tbody tr th:only-of-type {\n",
       "        vertical-align: middle;\n",
       "    }\n",
       "\n",
       "    .dataframe tbody tr th {\n",
       "        vertical-align: top;\n",
       "    }\n",
       "\n",
       "    .dataframe thead th {\n",
       "        text-align: right;\n",
       "    }\n",
       "</style>\n",
       "<table border=\"1\" class=\"dataframe\">\n",
       "  <thead>\n",
       "    <tr style=\"text-align: right;\">\n",
       "      <th></th>\n",
       "      <th>case:concept:name</th>\n",
       "      <th>accepted</th>\n",
       "    </tr>\n",
       "  </thead>\n",
       "  <tbody>\n",
       "    <tr>\n",
       "      <th>0</th>\n",
       "      <td>A</td>\n",
       "      <td>True</td>\n",
       "    </tr>\n",
       "    <tr>\n",
       "      <th>1</th>\n",
       "      <td>B</td>\n",
       "      <td>False</td>\n",
       "    </tr>\n",
       "    <tr>\n",
       "      <th>2</th>\n",
       "      <td>C</td>\n",
       "      <td>True</td>\n",
       "    </tr>\n",
       "    <tr>\n",
       "      <th>3</th>\n",
       "      <td>D</td>\n",
       "      <td>True</td>\n",
       "    </tr>\n",
       "    <tr>\n",
       "      <th>4</th>\n",
       "      <td>E</td>\n",
       "      <td>False</td>\n",
       "    </tr>\n",
       "    <tr>\n",
       "      <th>...</th>\n",
       "      <td>...</td>\n",
       "      <td>...</td>\n",
       "    </tr>\n",
       "    <tr>\n",
       "      <th>1045</th>\n",
       "      <td>HNA</td>\n",
       "      <td>True</td>\n",
       "    </tr>\n",
       "    <tr>\n",
       "      <th>1046</th>\n",
       "      <td>INA</td>\n",
       "      <td>False</td>\n",
       "    </tr>\n",
       "    <tr>\n",
       "      <th>1047</th>\n",
       "      <td>JNA</td>\n",
       "      <td>False</td>\n",
       "    </tr>\n",
       "    <tr>\n",
       "      <th>1048</th>\n",
       "      <td>KNA</td>\n",
       "      <td>True</td>\n",
       "    </tr>\n",
       "    <tr>\n",
       "      <th>1049</th>\n",
       "      <td>LNA</td>\n",
       "      <td>False</td>\n",
       "    </tr>\n",
       "  </tbody>\n",
       "</table>\n",
       "<p>1050 rows × 2 columns</p>\n",
       "</div>"
      ]
     },
     "execution_count": 9,
     "metadata": {},
     "output_type": "execute_result"
    }
   ],
   "execution_count": 9
  },
  {
   "cell_type": "markdown",
   "metadata": {},
   "source": [
    "### `eventually_a_then_b_then_c`\n",
    "\n",
    "This is a ternary template taking three activities as input. The corresponding LTLf formula is `F(a && F(b && F(c)))`."
   ]
  },
  {
   "cell_type": "code",
   "metadata": {
    "ExecuteTime": {
     "end_time": "2026-05-29T14:00:08.740176100Z",
     "start_time": "2026-05-29T14:00:07.444581600Z"
    }
   },
   "source": [
    "template = LTLTemplate('eventually_a_then_b_then_c')\n",
    "model = template.fill_template(['ER Registration', 'Leucocytes', 'CRP'])\n",
    "print(f\"Formula: {model.formula}\")\n",
    "analyzer = LTLAnalyzer(event_log, model)\n",
    "conf_check_res_df = analyzer.run()\n",
    "conf_check_res_df"
   ],
   "outputs": [
    {
     "name": "stdout",
     "output_type": "stream",
     "text": [
      "Formula: F(con_erregistration  && F(con_leucocytes  && F(con_crp)))\n"
     ]
    },
    {
     "data": {
      "text/plain": [
       "     case:concept:name  accepted\n",
       "0                    A      True\n",
       "1                    B      True\n",
       "2                    C      True\n",
       "3                    D      True\n",
       "4                    E     False\n",
       "...                ...       ...\n",
       "1045               HNA      True\n",
       "1046               INA     False\n",
       "1047               JNA     False\n",
       "1048               KNA      True\n",
       "1049               LNA     False\n",
       "\n",
       "[1050 rows x 2 columns]"
      ],
      "text/html": [
       "<div>\n",
       "<style scoped>\n",
       "    .dataframe tbody tr th:only-of-type {\n",
       "        vertical-align: middle;\n",
       "    }\n",
       "\n",
       "    .dataframe tbody tr th {\n",
       "        vertical-align: top;\n",
       "    }\n",
       "\n",
       "    .dataframe thead th {\n",
       "        text-align: right;\n",
       "    }\n",
       "</style>\n",
       "<table border=\"1\" class=\"dataframe\">\n",
       "  <thead>\n",
       "    <tr style=\"text-align: right;\">\n",
       "      <th></th>\n",
       "      <th>case:concept:name</th>\n",
       "      <th>accepted</th>\n",
       "    </tr>\n",
       "  </thead>\n",
       "  <tbody>\n",
       "    <tr>\n",
       "      <th>0</th>\n",
       "      <td>A</td>\n",
       "      <td>True</td>\n",
       "    </tr>\n",
       "    <tr>\n",
       "      <th>1</th>\n",
       "      <td>B</td>\n",
       "      <td>True</td>\n",
       "    </tr>\n",
       "    <tr>\n",
       "      <th>2</th>\n",
       "      <td>C</td>\n",
       "      <td>True</td>\n",
       "    </tr>\n",
       "    <tr>\n",
       "      <th>3</th>\n",
       "      <td>D</td>\n",
       "      <td>True</td>\n",
       "    </tr>\n",
       "    <tr>\n",
       "      <th>4</th>\n",
       "      <td>E</td>\n",
       "      <td>False</td>\n",
       "    </tr>\n",
       "    <tr>\n",
       "      <th>...</th>\n",
       "      <td>...</td>\n",
       "      <td>...</td>\n",
       "    </tr>\n",
       "    <tr>\n",
       "      <th>1045</th>\n",
       "      <td>HNA</td>\n",
       "      <td>True</td>\n",
       "    </tr>\n",
       "    <tr>\n",
       "      <th>1046</th>\n",
       "      <td>INA</td>\n",
       "      <td>False</td>\n",
       "    </tr>\n",
       "    <tr>\n",
       "      <th>1047</th>\n",
       "      <td>JNA</td>\n",
       "      <td>False</td>\n",
       "    </tr>\n",
       "    <tr>\n",
       "      <th>1048</th>\n",
       "      <td>KNA</td>\n",
       "      <td>True</td>\n",
       "    </tr>\n",
       "    <tr>\n",
       "      <th>1049</th>\n",
       "      <td>LNA</td>\n",
       "      <td>False</td>\n",
       "    </tr>\n",
       "  </tbody>\n",
       "</table>\n",
       "<p>1050 rows × 2 columns</p>\n",
       "</div>"
      ]
     },
     "execution_count": 10,
     "metadata": {},
     "output_type": "execute_result"
    }
   ],
   "execution_count": 10
  },
  {
   "cell_type": "markdown",
   "metadata": {},
   "source": [
    "### `eventually_a_next_b_next_c`\n",
    "\n",
    "This is a ternary template taking three activities as input. The corresponding LTLf formula is `F(a && X(b && X(c)))`."
   ]
  },
  {
   "cell_type": "code",
   "metadata": {
    "ExecuteTime": {
     "end_time": "2026-05-29T14:00:11.203993400Z",
     "start_time": "2026-05-29T14:00:09.698622400Z"
    }
   },
   "source": [
    "template = LTLTemplate('eventually_a_next_b_next_c')\n",
    "model = template.fill_template(['ER Registration', 'CRP', 'Leucocytes'])\n",
    "print(f\"Formula: {model.formula}\")\n",
    "analyzer = LTLAnalyzer(event_log, model)\n",
    "conf_check_res_df = analyzer.run()\n",
    "conf_check_res_df"
   ],
   "outputs": [
    {
     "name": "stdout",
     "output_type": "stream",
     "text": [
      "Formula: F(con_erregistration  && X[!](con_crp  && X[!](con_leucocytes)))\n"
     ]
    },
    {
     "data": {
      "text/plain": [
       "     case:concept:name  accepted\n",
       "0                    A     False\n",
       "1                    B     False\n",
       "2                    C     False\n",
       "3                    D     False\n",
       "4                    E     False\n",
       "...                ...       ...\n",
       "1045               HNA     False\n",
       "1046               INA     False\n",
       "1047               JNA     False\n",
       "1048               KNA     False\n",
       "1049               LNA     False\n",
       "\n",
       "[1050 rows x 2 columns]"
      ],
      "text/html": [
       "<div>\n",
       "<style scoped>\n",
       "    .dataframe tbody tr th:only-of-type {\n",
       "        vertical-align: middle;\n",
       "    }\n",
       "\n",
       "    .dataframe tbody tr th {\n",
       "        vertical-align: top;\n",
       "    }\n",
       "\n",
       "    .dataframe thead th {\n",
       "        text-align: right;\n",
       "    }\n",
       "</style>\n",
       "<table border=\"1\" class=\"dataframe\">\n",
       "  <thead>\n",
       "    <tr style=\"text-align: right;\">\n",
       "      <th></th>\n",
       "      <th>case:concept:name</th>\n",
       "      <th>accepted</th>\n",
       "    </tr>\n",
       "  </thead>\n",
       "  <tbody>\n",
       "    <tr>\n",
       "      <th>0</th>\n",
       "      <td>A</td>\n",
       "      <td>False</td>\n",
       "    </tr>\n",
       "    <tr>\n",
       "      <th>1</th>\n",
       "      <td>B</td>\n",
       "      <td>False</td>\n",
       "    </tr>\n",
       "    <tr>\n",
       "      <th>2</th>\n",
       "      <td>C</td>\n",
       "      <td>False</td>\n",
       "    </tr>\n",
       "    <tr>\n",
       "      <th>3</th>\n",
       "      <td>D</td>\n",
       "      <td>False</td>\n",
       "    </tr>\n",
       "    <tr>\n",
       "      <th>4</th>\n",
       "      <td>E</td>\n",
       "      <td>False</td>\n",
       "    </tr>\n",
       "    <tr>\n",
       "      <th>...</th>\n",
       "      <td>...</td>\n",
       "      <td>...</td>\n",
       "    </tr>\n",
       "    <tr>\n",
       "      <th>1045</th>\n",
       "      <td>HNA</td>\n",
       "      <td>False</td>\n",
       "    </tr>\n",
       "    <tr>\n",
       "      <th>1046</th>\n",
       "      <td>INA</td>\n",
       "      <td>False</td>\n",
       "    </tr>\n",
       "    <tr>\n",
       "      <th>1047</th>\n",
       "      <td>JNA</td>\n",
       "      <td>False</td>\n",
       "    </tr>\n",
       "    <tr>\n",
       "      <th>1048</th>\n",
       "      <td>KNA</td>\n",
       "      <td>False</td>\n",
       "    </tr>\n",
       "    <tr>\n",
       "      <th>1049</th>\n",
       "      <td>LNA</td>\n",
       "      <td>False</td>\n",
       "    </tr>\n",
       "  </tbody>\n",
       "</table>\n",
       "<p>1050 rows × 2 columns</p>\n",
       "</div>"
      ]
     },
     "execution_count": 11,
     "metadata": {},
     "output_type": "execute_result"
    }
   ],
   "execution_count": 11
  },
  {
   "cell_type": "markdown",
   "metadata": {},
   "source": [
    "## Conformance Checking with LTLf Templates Is First (Last)\n",
    "\n",
    "These templates follow the same structure as the one used for simple LTLf templates. The `fill_template` method takes a list of generic attributes and a list of attribute types that match the type of the attributes in the first list. If the type of the attribute is 'concept:name' then the second list can be omitted."
   ]
  },
  {
   "cell_type": "markdown",
   "metadata": {},
   "source": [
    "### `is_first_state_a`\n",
    "This formula identifies all traces where attribute A is performed in the first event."
   ]
  },
  {
   "cell_type": "code",
   "metadata": {
    "ExecuteTime": {
     "end_time": "2026-05-29T14:00:11.802244100Z",
     "start_time": "2026-05-29T14:00:11.257008200Z"
    }
   },
   "source": [
    "template: LTLTemplate = LTLTemplate('is_first_state_a')\n",
    "model : LTLModel = template.fill_template(['ER Registration'])\n",
    "print(f\"Formula: {model.formula}\")\n",
    "analyzer = LTLAnalyzer(event_log, model)\n",
    "conf_check_res_df = analyzer.run()\n",
    "conf_check_res_df"
   ],
   "outputs": [
    {
     "name": "stdout",
     "output_type": "stream",
     "text": [
      "Formula: con_erregistration\n"
     ]
    },
    {
     "data": {
      "text/plain": [
       "     case:concept:name  accepted\n",
       "0                    A      True\n",
       "1                    B      True\n",
       "2                    C      True\n",
       "3                    D      True\n",
       "4                    E      True\n",
       "...                ...       ...\n",
       "1045               HNA      True\n",
       "1046               INA      True\n",
       "1047               JNA      True\n",
       "1048               KNA      True\n",
       "1049               LNA      True\n",
       "\n",
       "[1050 rows x 2 columns]"
      ],
      "text/html": [
       "<div>\n",
       "<style scoped>\n",
       "    .dataframe tbody tr th:only-of-type {\n",
       "        vertical-align: middle;\n",
       "    }\n",
       "\n",
       "    .dataframe tbody tr th {\n",
       "        vertical-align: top;\n",
       "    }\n",
       "\n",
       "    .dataframe thead th {\n",
       "        text-align: right;\n",
       "    }\n",
       "</style>\n",
       "<table border=\"1\" class=\"dataframe\">\n",
       "  <thead>\n",
       "    <tr style=\"text-align: right;\">\n",
       "      <th></th>\n",
       "      <th>case:concept:name</th>\n",
       "      <th>accepted</th>\n",
       "    </tr>\n",
       "  </thead>\n",
       "  <tbody>\n",
       "    <tr>\n",
       "      <th>0</th>\n",
       "      <td>A</td>\n",
       "      <td>True</td>\n",
       "    </tr>\n",
       "    <tr>\n",
       "      <th>1</th>\n",
       "      <td>B</td>\n",
       "      <td>True</td>\n",
       "    </tr>\n",
       "    <tr>\n",
       "      <th>2</th>\n",
       "      <td>C</td>\n",
       "      <td>True</td>\n",
       "    </tr>\n",
       "    <tr>\n",
       "      <th>3</th>\n",
       "      <td>D</td>\n",
       "      <td>True</td>\n",
       "    </tr>\n",
       "    <tr>\n",
       "      <th>4</th>\n",
       "      <td>E</td>\n",
       "      <td>True</td>\n",
       "    </tr>\n",
       "    <tr>\n",
       "      <th>...</th>\n",
       "      <td>...</td>\n",
       "      <td>...</td>\n",
       "    </tr>\n",
       "    <tr>\n",
       "      <th>1045</th>\n",
       "      <td>HNA</td>\n",
       "      <td>True</td>\n",
       "    </tr>\n",
       "    <tr>\n",
       "      <th>1046</th>\n",
       "      <td>INA</td>\n",
       "      <td>True</td>\n",
       "    </tr>\n",
       "    <tr>\n",
       "      <th>1047</th>\n",
       "      <td>JNA</td>\n",
       "      <td>True</td>\n",
       "    </tr>\n",
       "    <tr>\n",
       "      <th>1048</th>\n",
       "      <td>KNA</td>\n",
       "      <td>True</td>\n",
       "    </tr>\n",
       "    <tr>\n",
       "      <th>1049</th>\n",
       "      <td>LNA</td>\n",
       "      <td>True</td>\n",
       "    </tr>\n",
       "  </tbody>\n",
       "</table>\n",
       "<p>1050 rows × 2 columns</p>\n",
       "</div>"
      ]
     },
     "execution_count": 12,
     "metadata": {},
     "output_type": "execute_result"
    }
   ],
   "execution_count": 12
  },
  {
   "cell_type": "markdown",
   "metadata": {},
   "source": [
    "### `is_second_state_a`\n",
    "This formula identifies all traces where attribute A is performed in the second event."
   ]
  },
  {
   "cell_type": "code",
   "metadata": {
    "ExecuteTime": {
     "end_time": "2026-05-29T14:00:13.418908900Z",
     "start_time": "2026-05-29T14:00:12.873240900Z"
    }
   },
   "source": [
    "template: LTLTemplate = LTLTemplate('is_second_state_a')\n",
    "model : LTLModel = template.fill_template(['ER Triage'])\n",
    "print(f\"Formula: {model.formula}\")\n",
    "analyzer = LTLAnalyzer(event_log, model)\n",
    "conf_check_res_df = analyzer.run()\n",
    "conf_check_res_df"
   ],
   "outputs": [
    {
     "name": "stdout",
     "output_type": "stream",
     "text": [
      "Formula: X[!](con_ertriage)\n"
     ]
    },
    {
     "data": {
      "text/plain": [
       "     case:concept:name  accepted\n",
       "0                    A     False\n",
       "1                    B      True\n",
       "2                    C      True\n",
       "3                    D      True\n",
       "4                    E      True\n",
       "...                ...       ...\n",
       "1045               HNA      True\n",
       "1046               INA      True\n",
       "1047               JNA      True\n",
       "1048               KNA      True\n",
       "1049               LNA      True\n",
       "\n",
       "[1050 rows x 2 columns]"
      ],
      "text/html": [
       "<div>\n",
       "<style scoped>\n",
       "    .dataframe tbody tr th:only-of-type {\n",
       "        vertical-align: middle;\n",
       "    }\n",
       "\n",
       "    .dataframe tbody tr th {\n",
       "        vertical-align: top;\n",
       "    }\n",
       "\n",
       "    .dataframe thead th {\n",
       "        text-align: right;\n",
       "    }\n",
       "</style>\n",
       "<table border=\"1\" class=\"dataframe\">\n",
       "  <thead>\n",
       "    <tr style=\"text-align: right;\">\n",
       "      <th></th>\n",
       "      <th>case:concept:name</th>\n",
       "      <th>accepted</th>\n",
       "    </tr>\n",
       "  </thead>\n",
       "  <tbody>\n",
       "    <tr>\n",
       "      <th>0</th>\n",
       "      <td>A</td>\n",
       "      <td>False</td>\n",
       "    </tr>\n",
       "    <tr>\n",
       "      <th>1</th>\n",
       "      <td>B</td>\n",
       "      <td>True</td>\n",
       "    </tr>\n",
       "    <tr>\n",
       "      <th>2</th>\n",
       "      <td>C</td>\n",
       "      <td>True</td>\n",
       "    </tr>\n",
       "    <tr>\n",
       "      <th>3</th>\n",
       "      <td>D</td>\n",
       "      <td>True</td>\n",
       "    </tr>\n",
       "    <tr>\n",
       "      <th>4</th>\n",
       "      <td>E</td>\n",
       "      <td>True</td>\n",
       "    </tr>\n",
       "    <tr>\n",
       "      <th>...</th>\n",
       "      <td>...</td>\n",
       "      <td>...</td>\n",
       "    </tr>\n",
       "    <tr>\n",
       "      <th>1045</th>\n",
       "      <td>HNA</td>\n",
       "      <td>True</td>\n",
       "    </tr>\n",
       "    <tr>\n",
       "      <th>1046</th>\n",
       "      <td>INA</td>\n",
       "      <td>True</td>\n",
       "    </tr>\n",
       "    <tr>\n",
       "      <th>1047</th>\n",
       "      <td>JNA</td>\n",
       "      <td>True</td>\n",
       "    </tr>\n",
       "    <tr>\n",
       "      <th>1048</th>\n",
       "      <td>KNA</td>\n",
       "      <td>True</td>\n",
       "    </tr>\n",
       "    <tr>\n",
       "      <th>1049</th>\n",
       "      <td>LNA</td>\n",
       "      <td>True</td>\n",
       "    </tr>\n",
       "  </tbody>\n",
       "</table>\n",
       "<p>1050 rows × 2 columns</p>\n",
       "</div>"
      ]
     },
     "execution_count": 13,
     "metadata": {},
     "output_type": "execute_result"
    }
   ],
   "execution_count": 13
  },
  {
   "cell_type": "markdown",
   "metadata": {},
   "source": [
    "### `is_third_state_a`\n",
    "This formula identifies all traces where attribute A is performed in the third event."
   ]
  },
  {
   "cell_type": "code",
   "metadata": {
    "ExecuteTime": {
     "end_time": "2026-05-29T14:00:14.087039700Z",
     "start_time": "2026-05-29T14:00:13.483260600Z"
    }
   },
   "source": [
    "template: LTLTemplate = LTLTemplate('is_third_state_a')\n",
    "model : LTLModel = template.fill_template(['ER Sepsis Triage'])\n",
    "print(f\"Formula: {model.formula}\")\n",
    "analyzer = LTLAnalyzer(event_log, model)\n",
    "conf_check_res_df = analyzer.run()\n",
    "conf_check_res_df"
   ],
   "outputs": [
    {
     "name": "stdout",
     "output_type": "stream",
     "text": [
      "Formula: X[!](X[!](con_ersepsistriage))\n"
     ]
    },
    {
     "data": {
      "text/plain": [
       "     case:concept:name  accepted\n",
       "0                    A     False\n",
       "1                    B     False\n",
       "2                    C      True\n",
       "3                    D      True\n",
       "4                    E      True\n",
       "...                ...       ...\n",
       "1045               HNA      True\n",
       "1046               INA      True\n",
       "1047               JNA      True\n",
       "1048               KNA      True\n",
       "1049               LNA      True\n",
       "\n",
       "[1050 rows x 2 columns]"
      ],
      "text/html": [
       "<div>\n",
       "<style scoped>\n",
       "    .dataframe tbody tr th:only-of-type {\n",
       "        vertical-align: middle;\n",
       "    }\n",
       "\n",
       "    .dataframe tbody tr th {\n",
       "        vertical-align: top;\n",
       "    }\n",
       "\n",
       "    .dataframe thead th {\n",
       "        text-align: right;\n",
       "    }\n",
       "</style>\n",
       "<table border=\"1\" class=\"dataframe\">\n",
       "  <thead>\n",
       "    <tr style=\"text-align: right;\">\n",
       "      <th></th>\n",
       "      <th>case:concept:name</th>\n",
       "      <th>accepted</th>\n",
       "    </tr>\n",
       "  </thead>\n",
       "  <tbody>\n",
       "    <tr>\n",
       "      <th>0</th>\n",
       "      <td>A</td>\n",
       "      <td>False</td>\n",
       "    </tr>\n",
       "    <tr>\n",
       "      <th>1</th>\n",
       "      <td>B</td>\n",
       "      <td>False</td>\n",
       "    </tr>\n",
       "    <tr>\n",
       "      <th>2</th>\n",
       "      <td>C</td>\n",
       "      <td>True</td>\n",
       "    </tr>\n",
       "    <tr>\n",
       "      <th>3</th>\n",
       "      <td>D</td>\n",
       "      <td>True</td>\n",
       "    </tr>\n",
       "    <tr>\n",
       "      <th>4</th>\n",
       "      <td>E</td>\n",
       "      <td>True</td>\n",
       "    </tr>\n",
       "    <tr>\n",
       "      <th>...</th>\n",
       "      <td>...</td>\n",
       "      <td>...</td>\n",
       "    </tr>\n",
       "    <tr>\n",
       "      <th>1045</th>\n",
       "      <td>HNA</td>\n",
       "      <td>True</td>\n",
       "    </tr>\n",
       "    <tr>\n",
       "      <th>1046</th>\n",
       "      <td>INA</td>\n",
       "      <td>True</td>\n",
       "    </tr>\n",
       "    <tr>\n",
       "      <th>1047</th>\n",
       "      <td>JNA</td>\n",
       "      <td>True</td>\n",
       "    </tr>\n",
       "    <tr>\n",
       "      <th>1048</th>\n",
       "      <td>KNA</td>\n",
       "      <td>True</td>\n",
       "    </tr>\n",
       "    <tr>\n",
       "      <th>1049</th>\n",
       "      <td>LNA</td>\n",
       "      <td>True</td>\n",
       "    </tr>\n",
       "  </tbody>\n",
       "</table>\n",
       "<p>1050 rows × 2 columns</p>\n",
       "</div>"
      ]
     },
     "execution_count": 14,
     "metadata": {},
     "output_type": "execute_result"
    }
   ],
   "execution_count": 14
  },
  {
   "cell_type": "markdown",
   "metadata": {},
   "source": [
    "### `last`\n",
    "This formula identifies all traces where the attribute is guaranteed to change in the very next event. This formula takes an empty list as parameter."
   ]
  },
  {
   "cell_type": "code",
   "metadata": {
    "ExecuteTime": {
     "end_time": "2026-05-29T14:00:15.596952300Z",
     "start_time": "2026-05-29T14:00:15.050621Z"
    }
   },
   "source": [
    "template: LTLTemplate = LTLTemplate('last')\n",
    "model : LTLModel = template.fill_template([])\n",
    "print(f\"Formula: {model.formula}\")\n",
    "analyzer = LTLAnalyzer(event_log, model)\n",
    "conf_check_res_df = analyzer.run()\n",
    "conf_check_res_df"
   ],
   "outputs": [
    {
     "name": "stdout",
     "output_type": "stream",
     "text": [
      "Formula: !(X[!](true))\n"
     ]
    },
    {
     "data": {
      "text/plain": [
       "     case:concept:name  accepted\n",
       "0                    A     False\n",
       "1                    B     False\n",
       "2                    C     False\n",
       "3                    D     False\n",
       "4                    E     False\n",
       "...                ...       ...\n",
       "1045               HNA     False\n",
       "1046               INA     False\n",
       "1047               JNA     False\n",
       "1048               KNA     False\n",
       "1049               LNA     False\n",
       "\n",
       "[1050 rows x 2 columns]"
      ],
      "text/html": [
       "<div>\n",
       "<style scoped>\n",
       "    .dataframe tbody tr th:only-of-type {\n",
       "        vertical-align: middle;\n",
       "    }\n",
       "\n",
       "    .dataframe tbody tr th {\n",
       "        vertical-align: top;\n",
       "    }\n",
       "\n",
       "    .dataframe thead th {\n",
       "        text-align: right;\n",
       "    }\n",
       "</style>\n",
       "<table border=\"1\" class=\"dataframe\">\n",
       "  <thead>\n",
       "    <tr style=\"text-align: right;\">\n",
       "      <th></th>\n",
       "      <th>case:concept:name</th>\n",
       "      <th>accepted</th>\n",
       "    </tr>\n",
       "  </thead>\n",
       "  <tbody>\n",
       "    <tr>\n",
       "      <th>0</th>\n",
       "      <td>A</td>\n",
       "      <td>False</td>\n",
       "    </tr>\n",
       "    <tr>\n",
       "      <th>1</th>\n",
       "      <td>B</td>\n",
       "      <td>False</td>\n",
       "    </tr>\n",
       "    <tr>\n",
       "      <th>2</th>\n",
       "      <td>C</td>\n",
       "      <td>False</td>\n",
       "    </tr>\n",
       "    <tr>\n",
       "      <th>3</th>\n",
       "      <td>D</td>\n",
       "      <td>False</td>\n",
       "    </tr>\n",
       "    <tr>\n",
       "      <th>4</th>\n",
       "      <td>E</td>\n",
       "      <td>False</td>\n",
       "    </tr>\n",
       "    <tr>\n",
       "      <th>...</th>\n",
       "      <td>...</td>\n",
       "      <td>...</td>\n",
       "    </tr>\n",
       "    <tr>\n",
       "      <th>1045</th>\n",
       "      <td>HNA</td>\n",
       "      <td>False</td>\n",
       "    </tr>\n",
       "    <tr>\n",
       "      <th>1046</th>\n",
       "      <td>INA</td>\n",
       "      <td>False</td>\n",
       "    </tr>\n",
       "    <tr>\n",
       "      <th>1047</th>\n",
       "      <td>JNA</td>\n",
       "      <td>False</td>\n",
       "    </tr>\n",
       "    <tr>\n",
       "      <th>1048</th>\n",
       "      <td>KNA</td>\n",
       "      <td>False</td>\n",
       "    </tr>\n",
       "    <tr>\n",
       "      <th>1049</th>\n",
       "      <td>LNA</td>\n",
       "      <td>False</td>\n",
       "    </tr>\n",
       "  </tbody>\n",
       "</table>\n",
       "<p>1050 rows × 2 columns</p>\n",
       "</div>"
      ]
     },
     "execution_count": 15,
     "metadata": {},
     "output_type": "execute_result"
    }
   ],
   "execution_count": 15
  },
  {
   "cell_type": "markdown",
   "metadata": {},
   "source": [
    "### `second_last`\n",
    "This formula identifies all traces where at some point, there will be a change in the activity, indicating that it is not always equal to its previous event. This formula takes an empty list as parameter."
   ]
  },
  {
   "cell_type": "code",
   "metadata": {
    "ExecuteTime": {
     "end_time": "2026-05-29T14:00:16.352249200Z",
     "start_time": "2026-05-29T14:00:15.771597Z"
    }
   },
   "source": [
    "template: LTLTemplate = LTLTemplate('second_last')\n",
    "model : LTLModel = template.fill_template([])\n",
    "print(f\"Formula: {model.formula}\")\n",
    "analyzer = LTLAnalyzer(event_log, model)\n",
    "conf_check_res_df = analyzer.run()\n",
    "conf_check_res_df"
   ],
   "outputs": [
    {
     "name": "stdout",
     "output_type": "stream",
     "text": [
      "Formula: X[!](!(X[!](true)))\n"
     ]
    },
    {
     "data": {
      "text/plain": [
       "     case:concept:name  accepted\n",
       "0                    A     False\n",
       "1                    B     False\n",
       "2                    C     False\n",
       "3                    D     False\n",
       "4                    E     False\n",
       "...                ...       ...\n",
       "1045               HNA     False\n",
       "1046               INA     False\n",
       "1047               JNA     False\n",
       "1048               KNA     False\n",
       "1049               LNA     False\n",
       "\n",
       "[1050 rows x 2 columns]"
      ],
      "text/html": [
       "<div>\n",
       "<style scoped>\n",
       "    .dataframe tbody tr th:only-of-type {\n",
       "        vertical-align: middle;\n",
       "    }\n",
       "\n",
       "    .dataframe tbody tr th {\n",
       "        vertical-align: top;\n",
       "    }\n",
       "\n",
       "    .dataframe thead th {\n",
       "        text-align: right;\n",
       "    }\n",
       "</style>\n",
       "<table border=\"1\" class=\"dataframe\">\n",
       "  <thead>\n",
       "    <tr style=\"text-align: right;\">\n",
       "      <th></th>\n",
       "      <th>case:concept:name</th>\n",
       "      <th>accepted</th>\n",
       "    </tr>\n",
       "  </thead>\n",
       "  <tbody>\n",
       "    <tr>\n",
       "      <th>0</th>\n",
       "      <td>A</td>\n",
       "      <td>False</td>\n",
       "    </tr>\n",
       "    <tr>\n",
       "      <th>1</th>\n",
       "      <td>B</td>\n",
       "      <td>False</td>\n",
       "    </tr>\n",
       "    <tr>\n",
       "      <th>2</th>\n",
       "      <td>C</td>\n",
       "      <td>False</td>\n",
       "    </tr>\n",
       "    <tr>\n",
       "      <th>3</th>\n",
       "      <td>D</td>\n",
       "      <td>False</td>\n",
       "    </tr>\n",
       "    <tr>\n",
       "      <th>4</th>\n",
       "      <td>E</td>\n",
       "      <td>False</td>\n",
       "    </tr>\n",
       "    <tr>\n",
       "      <th>...</th>\n",
       "      <td>...</td>\n",
       "      <td>...</td>\n",
       "    </tr>\n",
       "    <tr>\n",
       "      <th>1045</th>\n",
       "      <td>HNA</td>\n",
       "      <td>False</td>\n",
       "    </tr>\n",
       "    <tr>\n",
       "      <th>1046</th>\n",
       "      <td>INA</td>\n",
       "      <td>False</td>\n",
       "    </tr>\n",
       "    <tr>\n",
       "      <th>1047</th>\n",
       "      <td>JNA</td>\n",
       "      <td>False</td>\n",
       "    </tr>\n",
       "    <tr>\n",
       "      <th>1048</th>\n",
       "      <td>KNA</td>\n",
       "      <td>False</td>\n",
       "    </tr>\n",
       "    <tr>\n",
       "      <th>1049</th>\n",
       "      <td>LNA</td>\n",
       "      <td>False</td>\n",
       "    </tr>\n",
       "  </tbody>\n",
       "</table>\n",
       "<p>1050 rows × 2 columns</p>\n",
       "</div>"
      ]
     },
     "execution_count": 16,
     "metadata": {},
     "output_type": "execute_result"
    }
   ],
   "execution_count": 16
  },
  {
   "cell_type": "markdown",
   "metadata": {},
   "source": [
    "### `third_last`\n",
    "This formula identifies all traces where there will be a change in the activity in the very next time step and that this change will persist at least once more in the future. This formula takes an empty list as parameter."
   ]
  },
  {
   "cell_type": "code",
   "metadata": {
    "ExecuteTime": {
     "end_time": "2026-05-29T14:00:17.910550500Z",
     "start_time": "2026-05-29T14:00:17.307744800Z"
    }
   },
   "source": [
    "template: LTLTemplate = LTLTemplate('third_last')\n",
    "model : LTLModel = template.fill_template([])\n",
    "print(f\"Formula: {model.formula}\")\n",
    "analyzer = LTLAnalyzer(event_log, model)\n",
    "conf_check_res_df = analyzer.run()\n",
    "conf_check_res_df"
   ],
   "outputs": [
    {
     "name": "stdout",
     "output_type": "stream",
     "text": [
      "Formula: X[!](X[!](!(X[!](true))))\n"
     ]
    },
    {
     "data": {
      "text/plain": [
       "     case:concept:name  accepted\n",
       "0                    A     False\n",
       "1                    B     False\n",
       "2                    C     False\n",
       "3                    D     False\n",
       "4                    E     False\n",
       "...                ...       ...\n",
       "1045               HNA     False\n",
       "1046               INA      True\n",
       "1047               JNA      True\n",
       "1048               KNA     False\n",
       "1049               LNA      True\n",
       "\n",
       "[1050 rows x 2 columns]"
      ],
      "text/html": [
       "<div>\n",
       "<style scoped>\n",
       "    .dataframe tbody tr th:only-of-type {\n",
       "        vertical-align: middle;\n",
       "    }\n",
       "\n",
       "    .dataframe tbody tr th {\n",
       "        vertical-align: top;\n",
       "    }\n",
       "\n",
       "    .dataframe thead th {\n",
       "        text-align: right;\n",
       "    }\n",
       "</style>\n",
       "<table border=\"1\" class=\"dataframe\">\n",
       "  <thead>\n",
       "    <tr style=\"text-align: right;\">\n",
       "      <th></th>\n",
       "      <th>case:concept:name</th>\n",
       "      <th>accepted</th>\n",
       "    </tr>\n",
       "  </thead>\n",
       "  <tbody>\n",
       "    <tr>\n",
       "      <th>0</th>\n",
       "      <td>A</td>\n",
       "      <td>False</td>\n",
       "    </tr>\n",
       "    <tr>\n",
       "      <th>1</th>\n",
       "      <td>B</td>\n",
       "      <td>False</td>\n",
       "    </tr>\n",
       "    <tr>\n",
       "      <th>2</th>\n",
       "      <td>C</td>\n",
       "      <td>False</td>\n",
       "    </tr>\n",
       "    <tr>\n",
       "      <th>3</th>\n",
       "      <td>D</td>\n",
       "      <td>False</td>\n",
       "    </tr>\n",
       "    <tr>\n",
       "      <th>4</th>\n",
       "      <td>E</td>\n",
       "      <td>False</td>\n",
       "    </tr>\n",
       "    <tr>\n",
       "      <th>...</th>\n",
       "      <td>...</td>\n",
       "      <td>...</td>\n",
       "    </tr>\n",
       "    <tr>\n",
       "      <th>1045</th>\n",
       "      <td>HNA</td>\n",
       "      <td>False</td>\n",
       "    </tr>\n",
       "    <tr>\n",
       "      <th>1046</th>\n",
       "      <td>INA</td>\n",
       "      <td>True</td>\n",
       "    </tr>\n",
       "    <tr>\n",
       "      <th>1047</th>\n",
       "      <td>JNA</td>\n",
       "      <td>True</td>\n",
       "    </tr>\n",
       "    <tr>\n",
       "      <th>1048</th>\n",
       "      <td>KNA</td>\n",
       "      <td>False</td>\n",
       "    </tr>\n",
       "    <tr>\n",
       "      <th>1049</th>\n",
       "      <td>LNA</td>\n",
       "      <td>True</td>\n",
       "    </tr>\n",
       "  </tbody>\n",
       "</table>\n",
       "<p>1050 rows × 2 columns</p>\n",
       "</div>"
      ]
     },
     "execution_count": 17,
     "metadata": {},
     "output_type": "execute_result"
    }
   ],
   "execution_count": 17
  },
  {
   "cell_type": "markdown",
   "metadata": {},
   "source": [
    "### `is_last_state_a`\n",
    "This formula identifies all traces where attribute A is performed in the last event."
   ]
  },
  {
   "cell_type": "code",
   "metadata": {
    "ExecuteTime": {
     "end_time": "2026-05-29T14:00:19.192552Z",
     "start_time": "2026-05-29T14:00:17.965215800Z"
    }
   },
   "source": [
    "template: LTLTemplate = LTLTemplate('is_last_state_a')\n",
    "model : LTLModel = template.fill_template(['Release A'])\n",
    "print(f\"Formula: {model.formula}\")\n",
    "analyzer = LTLAnalyzer(event_log, model)\n",
    "conf_check_res_df = analyzer.run()\n",
    "conf_check_res_df"
   ],
   "outputs": [
    {
     "name": "stdout",
     "output_type": "stream",
     "text": [
      "Formula: F(con_releasea  &&  !(X[!](true)))\n"
     ]
    },
    {
     "data": {
      "text/plain": [
       "     case:concept:name  accepted\n",
       "0                    A      True\n",
       "1                    B      True\n",
       "2                    C      True\n",
       "3                    D     False\n",
       "4                    E     False\n",
       "...                ...       ...\n",
       "1045               HNA      True\n",
       "1046               INA     False\n",
       "1047               JNA     False\n",
       "1048               KNA      True\n",
       "1049               LNA     False\n",
       "\n",
       "[1050 rows x 2 columns]"
      ],
      "text/html": [
       "<div>\n",
       "<style scoped>\n",
       "    .dataframe tbody tr th:only-of-type {\n",
       "        vertical-align: middle;\n",
       "    }\n",
       "\n",
       "    .dataframe tbody tr th {\n",
       "        vertical-align: top;\n",
       "    }\n",
       "\n",
       "    .dataframe thead th {\n",
       "        text-align: right;\n",
       "    }\n",
       "</style>\n",
       "<table border=\"1\" class=\"dataframe\">\n",
       "  <thead>\n",
       "    <tr style=\"text-align: right;\">\n",
       "      <th></th>\n",
       "      <th>case:concept:name</th>\n",
       "      <th>accepted</th>\n",
       "    </tr>\n",
       "  </thead>\n",
       "  <tbody>\n",
       "    <tr>\n",
       "      <th>0</th>\n",
       "      <td>A</td>\n",
       "      <td>True</td>\n",
       "    </tr>\n",
       "    <tr>\n",
       "      <th>1</th>\n",
       "      <td>B</td>\n",
       "      <td>True</td>\n",
       "    </tr>\n",
       "    <tr>\n",
       "      <th>2</th>\n",
       "      <td>C</td>\n",
       "      <td>True</td>\n",
       "    </tr>\n",
       "    <tr>\n",
       "      <th>3</th>\n",
       "      <td>D</td>\n",
       "      <td>False</td>\n",
       "    </tr>\n",
       "    <tr>\n",
       "      <th>4</th>\n",
       "      <td>E</td>\n",
       "      <td>False</td>\n",
       "    </tr>\n",
       "    <tr>\n",
       "      <th>...</th>\n",
       "      <td>...</td>\n",
       "      <td>...</td>\n",
       "    </tr>\n",
       "    <tr>\n",
       "      <th>1045</th>\n",
       "      <td>HNA</td>\n",
       "      <td>True</td>\n",
       "    </tr>\n",
       "    <tr>\n",
       "      <th>1046</th>\n",
       "      <td>INA</td>\n",
       "      <td>False</td>\n",
       "    </tr>\n",
       "    <tr>\n",
       "      <th>1047</th>\n",
       "      <td>JNA</td>\n",
       "      <td>False</td>\n",
       "    </tr>\n",
       "    <tr>\n",
       "      <th>1048</th>\n",
       "      <td>KNA</td>\n",
       "      <td>True</td>\n",
       "    </tr>\n",
       "    <tr>\n",
       "      <th>1049</th>\n",
       "      <td>LNA</td>\n",
       "      <td>False</td>\n",
       "    </tr>\n",
       "  </tbody>\n",
       "</table>\n",
       "<p>1050 rows × 2 columns</p>\n",
       "</div>"
      ]
     },
     "execution_count": 18,
     "metadata": {},
     "output_type": "execute_result"
    }
   ],
   "execution_count": 18
  },
  {
   "cell_type": "markdown",
   "metadata": {},
   "source": [
    "### `is_second_last_state_a`\n",
    "This formula identifies all traces where attribute A is performed in the penultimate event."
   ]
  },
  {
   "cell_type": "code",
   "metadata": {
    "ExecuteTime": {
     "end_time": "2026-05-29T14:00:21.418096300Z",
     "start_time": "2026-05-29T14:00:20.250364600Z"
    }
   },
   "source": [
    "template: LTLTemplate = LTLTemplate('is_second_last_state_a')\n",
    "model : LTLModel = template.fill_template(['Leucocytes'])\n",
    "print(f\"Formula: {model.formula}\")\n",
    "analyzer = LTLAnalyzer(event_log, model)\n",
    "conf_check_res_df = analyzer.run()\n",
    "conf_check_res_df"
   ],
   "outputs": [
    {
     "name": "stdout",
     "output_type": "stream",
     "text": [
      "Formula: F(con_leucocytes  && X[!](!(X[!](true))))\n"
     ]
    },
    {
     "data": {
      "text/plain": [
       "     case:concept:name  accepted\n",
       "0                    A      True\n",
       "1                    B     False\n",
       "2                    C     False\n",
       "3                    D     False\n",
       "4                    E     False\n",
       "...                ...       ...\n",
       "1045               HNA     False\n",
       "1046               INA     False\n",
       "1047               JNA     False\n",
       "1048               KNA     False\n",
       "1049               LNA     False\n",
       "\n",
       "[1050 rows x 2 columns]"
      ],
      "text/html": [
       "<div>\n",
       "<style scoped>\n",
       "    .dataframe tbody tr th:only-of-type {\n",
       "        vertical-align: middle;\n",
       "    }\n",
       "\n",
       "    .dataframe tbody tr th {\n",
       "        vertical-align: top;\n",
       "    }\n",
       "\n",
       "    .dataframe thead th {\n",
       "        text-align: right;\n",
       "    }\n",
       "</style>\n",
       "<table border=\"1\" class=\"dataframe\">\n",
       "  <thead>\n",
       "    <tr style=\"text-align: right;\">\n",
       "      <th></th>\n",
       "      <th>case:concept:name</th>\n",
       "      <th>accepted</th>\n",
       "    </tr>\n",
       "  </thead>\n",
       "  <tbody>\n",
       "    <tr>\n",
       "      <th>0</th>\n",
       "      <td>A</td>\n",
       "      <td>True</td>\n",
       "    </tr>\n",
       "    <tr>\n",
       "      <th>1</th>\n",
       "      <td>B</td>\n",
       "      <td>False</td>\n",
       "    </tr>\n",
       "    <tr>\n",
       "      <th>2</th>\n",
       "      <td>C</td>\n",
       "      <td>False</td>\n",
       "    </tr>\n",
       "    <tr>\n",
       "      <th>3</th>\n",
       "      <td>D</td>\n",
       "      <td>False</td>\n",
       "    </tr>\n",
       "    <tr>\n",
       "      <th>4</th>\n",
       "      <td>E</td>\n",
       "      <td>False</td>\n",
       "    </tr>\n",
       "    <tr>\n",
       "      <th>...</th>\n",
       "      <td>...</td>\n",
       "      <td>...</td>\n",
       "    </tr>\n",
       "    <tr>\n",
       "      <th>1045</th>\n",
       "      <td>HNA</td>\n",
       "      <td>False</td>\n",
       "    </tr>\n",
       "    <tr>\n",
       "      <th>1046</th>\n",
       "      <td>INA</td>\n",
       "      <td>False</td>\n",
       "    </tr>\n",
       "    <tr>\n",
       "      <th>1047</th>\n",
       "      <td>JNA</td>\n",
       "      <td>False</td>\n",
       "    </tr>\n",
       "    <tr>\n",
       "      <th>1048</th>\n",
       "      <td>KNA</td>\n",
       "      <td>False</td>\n",
       "    </tr>\n",
       "    <tr>\n",
       "      <th>1049</th>\n",
       "      <td>LNA</td>\n",
       "      <td>False</td>\n",
       "    </tr>\n",
       "  </tbody>\n",
       "</table>\n",
       "<p>1050 rows × 2 columns</p>\n",
       "</div>"
      ]
     },
     "execution_count": 19,
     "metadata": {},
     "output_type": "execute_result"
    }
   ],
   "execution_count": 19
  },
  {
   "cell_type": "markdown",
   "metadata": {},
   "source": [
    "### `is_third_last_state_a`\n",
    "This formula identifies all traces where attribute A is performed in the third-last event."
   ]
  },
  {
   "cell_type": "code",
   "metadata": {
    "ExecuteTime": {
     "end_time": "2026-05-29T14:00:22.705931900Z",
     "start_time": "2026-05-29T14:00:21.458607Z"
    }
   },
   "source": [
    "template: LTLTemplate = LTLTemplate('is_third_last_state_a')\n",
    "model : LTLModel = template.fill_template(['CRP'])\n",
    "print(f\"Formula: {model.formula}\")\n",
    "analyzer = LTLAnalyzer(event_log, model)\n",
    "conf_check_res_df = analyzer.run()\n",
    "conf_check_res_df"
   ],
   "outputs": [
    {
     "name": "stdout",
     "output_type": "stream",
     "text": [
      "Formula: F(con_crp  && X[!](X[!](!(X[!](true)))))\n"
     ]
    },
    {
     "data": {
      "text/plain": [
       "     case:concept:name  accepted\n",
       "0                    A      True\n",
       "1                    B      True\n",
       "2                    C     False\n",
       "3                    D      True\n",
       "4                    E     False\n",
       "...                ...       ...\n",
       "1045               HNA     False\n",
       "1046               INA     False\n",
       "1047               JNA     False\n",
       "1048               KNA     False\n",
       "1049               LNA     False\n",
       "\n",
       "[1050 rows x 2 columns]"
      ],
      "text/html": [
       "<div>\n",
       "<style scoped>\n",
       "    .dataframe tbody tr th:only-of-type {\n",
       "        vertical-align: middle;\n",
       "    }\n",
       "\n",
       "    .dataframe tbody tr th {\n",
       "        vertical-align: top;\n",
       "    }\n",
       "\n",
       "    .dataframe thead th {\n",
       "        text-align: right;\n",
       "    }\n",
       "</style>\n",
       "<table border=\"1\" class=\"dataframe\">\n",
       "  <thead>\n",
       "    <tr style=\"text-align: right;\">\n",
       "      <th></th>\n",
       "      <th>case:concept:name</th>\n",
       "      <th>accepted</th>\n",
       "    </tr>\n",
       "  </thead>\n",
       "  <tbody>\n",
       "    <tr>\n",
       "      <th>0</th>\n",
       "      <td>A</td>\n",
       "      <td>True</td>\n",
       "    </tr>\n",
       "    <tr>\n",
       "      <th>1</th>\n",
       "      <td>B</td>\n",
       "      <td>True</td>\n",
       "    </tr>\n",
       "    <tr>\n",
       "      <th>2</th>\n",
       "      <td>C</td>\n",
       "      <td>False</td>\n",
       "    </tr>\n",
       "    <tr>\n",
       "      <th>3</th>\n",
       "      <td>D</td>\n",
       "      <td>True</td>\n",
       "    </tr>\n",
       "    <tr>\n",
       "      <th>4</th>\n",
       "      <td>E</td>\n",
       "      <td>False</td>\n",
       "    </tr>\n",
       "    <tr>\n",
       "      <th>...</th>\n",
       "      <td>...</td>\n",
       "      <td>...</td>\n",
       "    </tr>\n",
       "    <tr>\n",
       "      <th>1045</th>\n",
       "      <td>HNA</td>\n",
       "      <td>False</td>\n",
       "    </tr>\n",
       "    <tr>\n",
       "      <th>1046</th>\n",
       "      <td>INA</td>\n",
       "      <td>False</td>\n",
       "    </tr>\n",
       "    <tr>\n",
       "      <th>1047</th>\n",
       "      <td>JNA</td>\n",
       "      <td>False</td>\n",
       "    </tr>\n",
       "    <tr>\n",
       "      <th>1048</th>\n",
       "      <td>KNA</td>\n",
       "      <td>False</td>\n",
       "    </tr>\n",
       "    <tr>\n",
       "      <th>1049</th>\n",
       "      <td>LNA</td>\n",
       "      <td>False</td>\n",
       "    </tr>\n",
       "  </tbody>\n",
       "</table>\n",
       "<p>1050 rows × 2 columns</p>\n",
       "</div>"
      ]
     },
     "execution_count": 20,
     "metadata": {},
     "output_type": "execute_result"
    }
   ],
   "execution_count": 20
  },
  {
   "cell_type": "markdown",
   "metadata": {},
   "source": [
    "## Conformance Checking with LTLf Templates with multiple attributes\n",
    "\n",
    "For these templates, the `fill_template` method takes a list of generic attributes (in string format) and a list of  attribute types (also strings) as parameters. The order of the elements of these two lists is important. For each template, the instantiated template formula and its corresponding checking in the input log will be computed."
   ]
  },
  {
   "cell_type": "markdown",
   "metadata": {},
   "source": [
    "### `p_does_a`"
   ]
  },
  {
   "cell_type": "code",
   "metadata": {
    "ExecuteTime": {
     "end_time": "2026-05-29T14:00:24.445382900Z",
     "start_time": "2026-05-29T14:00:23.668652900Z"
    }
   },
   "source": [
    "template: LTLTemplate = LTLTemplate('p_does_a')\n",
    "model : LTLModel = template.fill_template(['A', 'ER Registration'], attr_type=['org:group', 'concept:name'])\n",
    "print(f\"Formula: {model.formula}\")\n",
    "analyzer = LTLAnalyzer(event_log, model)\n",
    "conf_check_res_df = analyzer.run()\n",
    "conf_check_res_df"
   ],
   "outputs": [
    {
     "name": "stdout",
     "output_type": "stream",
     "text": [
      "Formula: F(org_a  && con_erregistration)\n"
     ]
    },
    {
     "data": {
      "text/plain": [
       "     case:concept:name  accepted\n",
       "0                    A      True\n",
       "1                    B      True\n",
       "2                    C      True\n",
       "3                    D      True\n",
       "4                    E      True\n",
       "...                ...       ...\n",
       "1045               HNA      True\n",
       "1046               INA      True\n",
       "1047               JNA      True\n",
       "1048               KNA      True\n",
       "1049               LNA     False\n",
       "\n",
       "[1050 rows x 2 columns]"
      ],
      "text/html": [
       "<div>\n",
       "<style scoped>\n",
       "    .dataframe tbody tr th:only-of-type {\n",
       "        vertical-align: middle;\n",
       "    }\n",
       "\n",
       "    .dataframe tbody tr th {\n",
       "        vertical-align: top;\n",
       "    }\n",
       "\n",
       "    .dataframe thead th {\n",
       "        text-align: right;\n",
       "    }\n",
       "</style>\n",
       "<table border=\"1\" class=\"dataframe\">\n",
       "  <thead>\n",
       "    <tr style=\"text-align: right;\">\n",
       "      <th></th>\n",
       "      <th>case:concept:name</th>\n",
       "      <th>accepted</th>\n",
       "    </tr>\n",
       "  </thead>\n",
       "  <tbody>\n",
       "    <tr>\n",
       "      <th>0</th>\n",
       "      <td>A</td>\n",
       "      <td>True</td>\n",
       "    </tr>\n",
       "    <tr>\n",
       "      <th>1</th>\n",
       "      <td>B</td>\n",
       "      <td>True</td>\n",
       "    </tr>\n",
       "    <tr>\n",
       "      <th>2</th>\n",
       "      <td>C</td>\n",
       "      <td>True</td>\n",
       "    </tr>\n",
       "    <tr>\n",
       "      <th>3</th>\n",
       "      <td>D</td>\n",
       "      <td>True</td>\n",
       "    </tr>\n",
       "    <tr>\n",
       "      <th>4</th>\n",
       "      <td>E</td>\n",
       "      <td>True</td>\n",
       "    </tr>\n",
       "    <tr>\n",
       "      <th>...</th>\n",
       "      <td>...</td>\n",
       "      <td>...</td>\n",
       "    </tr>\n",
       "    <tr>\n",
       "      <th>1045</th>\n",
       "      <td>HNA</td>\n",
       "      <td>True</td>\n",
       "    </tr>\n",
       "    <tr>\n",
       "      <th>1046</th>\n",
       "      <td>INA</td>\n",
       "      <td>True</td>\n",
       "    </tr>\n",
       "    <tr>\n",
       "      <th>1047</th>\n",
       "      <td>JNA</td>\n",
       "      <td>True</td>\n",
       "    </tr>\n",
       "    <tr>\n",
       "      <th>1048</th>\n",
       "      <td>KNA</td>\n",
       "      <td>True</td>\n",
       "    </tr>\n",
       "    <tr>\n",
       "      <th>1049</th>\n",
       "      <td>LNA</td>\n",
       "      <td>False</td>\n",
       "    </tr>\n",
       "  </tbody>\n",
       "</table>\n",
       "<p>1050 rows × 2 columns</p>\n",
       "</div>"
      ]
     },
     "execution_count": 21,
     "metadata": {},
     "output_type": "execute_result"
    }
   ],
   "execution_count": 21
  },
  {
   "cell_type": "markdown",
   "metadata": {},
   "source": [
    "### `a_is_done_by_p_and_q`"
   ]
  },
  {
   "cell_type": "code",
   "metadata": {
    "scrolled": true,
    "ExecuteTime": {
     "end_time": "2026-05-29T14:00:26.916144200Z",
     "start_time": "2026-05-29T14:00:24.498459400Z"
    }
   },
   "source": [
    "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: {model.formula}\")\n",
    "analyzer = LTLAnalyzer(event_log, model)\n",
    "conf_check_res_df = analyzer.run()\n",
    "conf_check_res_df"
   ],
   "outputs": [
    {
     "name": "stdout",
     "output_type": "stream",
     "text": [
      "Formula: (F(F(org_a  && con_erregistration))  && F(F(org_b  && con_erregistration)))\n"
     ]
    },
    {
     "data": {
      "text/plain": [
       "     case:concept:name  accepted\n",
       "0                    A     False\n",
       "1                    B     False\n",
       "2                    C     False\n",
       "3                    D     False\n",
       "4                    E     False\n",
       "...                ...       ...\n",
       "1045               HNA     False\n",
       "1046               INA     False\n",
       "1047               JNA     False\n",
       "1048               KNA     False\n",
       "1049               LNA     False\n",
       "\n",
       "[1050 rows x 2 columns]"
      ],
      "text/html": [
       "<div>\n",
       "<style scoped>\n",
       "    .dataframe tbody tr th:only-of-type {\n",
       "        vertical-align: middle;\n",
       "    }\n",
       "\n",
       "    .dataframe tbody tr th {\n",
       "        vertical-align: top;\n",
       "    }\n",
       "\n",
       "    .dataframe thead th {\n",
       "        text-align: right;\n",
       "    }\n",
       "</style>\n",
       "<table border=\"1\" class=\"dataframe\">\n",
       "  <thead>\n",
       "    <tr style=\"text-align: right;\">\n",
       "      <th></th>\n",
       "      <th>case:concept:name</th>\n",
       "      <th>accepted</th>\n",
       "    </tr>\n",
       "  </thead>\n",
       "  <tbody>\n",
       "    <tr>\n",
       "      <th>0</th>\n",
       "      <td>A</td>\n",
       "      <td>False</td>\n",
       "    </tr>\n",
       "    <tr>\n",
       "      <th>1</th>\n",
       "      <td>B</td>\n",
       "      <td>False</td>\n",
       "    </tr>\n",
       "    <tr>\n",
       "      <th>2</th>\n",
       "      <td>C</td>\n",
       "      <td>False</td>\n",
       "    </tr>\n",
       "    <tr>\n",
       "      <th>3</th>\n",
       "      <td>D</td>\n",
       "      <td>False</td>\n",
       "    </tr>\n",
       "    <tr>\n",
       "      <th>4</th>\n",
       "      <td>E</td>\n",
       "      <td>False</td>\n",
       "    </tr>\n",
       "    <tr>\n",
       "      <th>...</th>\n",
       "      <td>...</td>\n",
       "      <td>...</td>\n",
       "    </tr>\n",
       "    <tr>\n",
       "      <th>1045</th>\n",
       "      <td>HNA</td>\n",
       "      <td>False</td>\n",
       "    </tr>\n",
       "    <tr>\n",
       "      <th>1046</th>\n",
       "      <td>INA</td>\n",
       "      <td>False</td>\n",
       "    </tr>\n",
       "    <tr>\n",
       "      <th>1047</th>\n",
       "      <td>JNA</td>\n",
       "      <td>False</td>\n",
       "    </tr>\n",
       "    <tr>\n",
       "      <th>1048</th>\n",
       "      <td>KNA</td>\n",
       "      <td>False</td>\n",
       "    </tr>\n",
       "    <tr>\n",
       "      <th>1049</th>\n",
       "      <td>LNA</td>\n",
       "      <td>False</td>\n",
       "    </tr>\n",
       "  </tbody>\n",
       "</table>\n",
       "<p>1050 rows × 2 columns</p>\n",
       "</div>"
      ]
     },
     "execution_count": 22,
     "metadata": {},
     "output_type": "execute_result"
    }
   ],
   "execution_count": 22
  },
  {
   "cell_type": "markdown",
   "metadata": {},
   "source": [
    "### `p_does_a_and_b`"
   ]
  },
  {
   "cell_type": "code",
   "metadata": {
    "ExecuteTime": {
     "end_time": "2026-05-29T14:00:30.348710Z",
     "start_time": "2026-05-29T14:00:27.867744100Z"
    }
   },
   "source": [
    "template: LTLTemplate = LTLTemplate('p_does_a_and_b')\n",
    "model : LTLModel = template.fill_template(['A', 'ER Registration', 'Leucocytes'], attr_type=['org:group', 'concept:name'])\n",
    "print(f\"Formula: {model.formula}\")\n",
    "analyzer = LTLAnalyzer(event_log, model)\n",
    "conf_check_res_df = analyzer.run()\n",
    "conf_check_res_df"
   ],
   "outputs": [
    {
     "name": "stdout",
     "output_type": "stream",
     "text": [
      "Formula: (F(F(org_a  &&  con_erregistration))  && F(F(org_a  &&  con_leucocytes)))\n"
     ]
    },
    {
     "data": {
      "text/plain": [
       "     case:concept:name  accepted\n",
       "0                    A     False\n",
       "1                    B     False\n",
       "2                    C     False\n",
       "3                    D     False\n",
       "4                    E     False\n",
       "...                ...       ...\n",
       "1045               HNA     False\n",
       "1046               INA     False\n",
       "1047               JNA     False\n",
       "1048               KNA     False\n",
       "1049               LNA     False\n",
       "\n",
       "[1050 rows x 2 columns]"
      ],
      "text/html": [
       "<div>\n",
       "<style scoped>\n",
       "    .dataframe tbody tr th:only-of-type {\n",
       "        vertical-align: middle;\n",
       "    }\n",
       "\n",
       "    .dataframe tbody tr th {\n",
       "        vertical-align: top;\n",
       "    }\n",
       "\n",
       "    .dataframe thead th {\n",
       "        text-align: right;\n",
       "    }\n",
       "</style>\n",
       "<table border=\"1\" class=\"dataframe\">\n",
       "  <thead>\n",
       "    <tr style=\"text-align: right;\">\n",
       "      <th></th>\n",
       "      <th>case:concept:name</th>\n",
       "      <th>accepted</th>\n",
       "    </tr>\n",
       "  </thead>\n",
       "  <tbody>\n",
       "    <tr>\n",
       "      <th>0</th>\n",
       "      <td>A</td>\n",
       "      <td>False</td>\n",
       "    </tr>\n",
       "    <tr>\n",
       "      <th>1</th>\n",
       "      <td>B</td>\n",
       "      <td>False</td>\n",
       "    </tr>\n",
       "    <tr>\n",
       "      <th>2</th>\n",
       "      <td>C</td>\n",
       "      <td>False</td>\n",
       "    </tr>\n",
       "    <tr>\n",
       "      <th>3</th>\n",
       "      <td>D</td>\n",
       "      <td>False</td>\n",
       "    </tr>\n",
       "    <tr>\n",
       "      <th>4</th>\n",
       "      <td>E</td>\n",
       "      <td>False</td>\n",
       "    </tr>\n",
       "    <tr>\n",
       "      <th>...</th>\n",
       "      <td>...</td>\n",
       "      <td>...</td>\n",
       "    </tr>\n",
       "    <tr>\n",
       "      <th>1045</th>\n",
       "      <td>HNA</td>\n",
       "      <td>False</td>\n",
       "    </tr>\n",
       "    <tr>\n",
       "      <th>1046</th>\n",
       "      <td>INA</td>\n",
       "      <td>False</td>\n",
       "    </tr>\n",
       "    <tr>\n",
       "      <th>1047</th>\n",
       "      <td>JNA</td>\n",
       "      <td>False</td>\n",
       "    </tr>\n",
       "    <tr>\n",
       "      <th>1048</th>\n",
       "      <td>KNA</td>\n",
       "      <td>False</td>\n",
       "    </tr>\n",
       "    <tr>\n",
       "      <th>1049</th>\n",
       "      <td>LNA</td>\n",
       "      <td>False</td>\n",
       "    </tr>\n",
       "  </tbody>\n",
       "</table>\n",
       "<p>1050 rows × 2 columns</p>\n",
       "</div>"
      ]
     },
     "execution_count": 23,
     "metadata": {},
     "output_type": "execute_result"
    }
   ],
   "execution_count": 23
  },
  {
   "cell_type": "markdown",
   "metadata": {},
   "source": [
    "### `p_does_a_and_then_b`"
   ]
  },
  {
   "cell_type": "code",
   "metadata": {
    "ExecuteTime": {
     "end_time": "2026-05-29T14:00:32.823318900Z",
     "start_time": "2026-05-29T14:00:30.403728900Z"
    }
   },
   "source": [
    "template: LTLTemplate = LTLTemplate('p_does_a_and_then_b')\n",
    "model : LTLModel = template.fill_template(['A', 'ER Registration', 'Leucocytes'], attr_type=['org:group', 'concept:name'])\n",
    "print(f\"Formula: {model.formula}\")\n",
    "analyzer = LTLAnalyzer(event_log, model)\n",
    "conf_check_res_df = analyzer.run()\n",
    "conf_check_res_df"
   ],
   "outputs": [
    {
     "name": "stdout",
     "output_type": "stream",
     "text": [
      "Formula: F((F(org_a  && con_erregistration)  && X[!](F(org_a  && con_leucocytes))))\n"
     ]
    },
    {
     "data": {
      "text/plain": [
       "     case:concept:name  accepted\n",
       "0                    A     False\n",
       "1                    B     False\n",
       "2                    C     False\n",
       "3                    D     False\n",
       "4                    E     False\n",
       "...                ...       ...\n",
       "1045               HNA     False\n",
       "1046               INA     False\n",
       "1047               JNA     False\n",
       "1048               KNA     False\n",
       "1049               LNA     False\n",
       "\n",
       "[1050 rows x 2 columns]"
      ],
      "text/html": [
       "<div>\n",
       "<style scoped>\n",
       "    .dataframe tbody tr th:only-of-type {\n",
       "        vertical-align: middle;\n",
       "    }\n",
       "\n",
       "    .dataframe tbody tr th {\n",
       "        vertical-align: top;\n",
       "    }\n",
       "\n",
       "    .dataframe thead th {\n",
       "        text-align: right;\n",
       "    }\n",
       "</style>\n",
       "<table border=\"1\" class=\"dataframe\">\n",
       "  <thead>\n",
       "    <tr style=\"text-align: right;\">\n",
       "      <th></th>\n",
       "      <th>case:concept:name</th>\n",
       "      <th>accepted</th>\n",
       "    </tr>\n",
       "  </thead>\n",
       "  <tbody>\n",
       "    <tr>\n",
       "      <th>0</th>\n",
       "      <td>A</td>\n",
       "      <td>False</td>\n",
       "    </tr>\n",
       "    <tr>\n",
       "      <th>1</th>\n",
       "      <td>B</td>\n",
       "      <td>False</td>\n",
       "    </tr>\n",
       "    <tr>\n",
       "      <th>2</th>\n",
       "      <td>C</td>\n",
       "      <td>False</td>\n",
       "    </tr>\n",
       "    <tr>\n",
       "      <th>3</th>\n",
       "      <td>D</td>\n",
       "      <td>False</td>\n",
       "    </tr>\n",
       "    <tr>\n",
       "      <th>4</th>\n",
       "      <td>E</td>\n",
       "      <td>False</td>\n",
       "    </tr>\n",
       "    <tr>\n",
       "      <th>...</th>\n",
       "      <td>...</td>\n",
       "      <td>...</td>\n",
       "    </tr>\n",
       "    <tr>\n",
       "      <th>1045</th>\n",
       "      <td>HNA</td>\n",
       "      <td>False</td>\n",
       "    </tr>\n",
       "    <tr>\n",
       "      <th>1046</th>\n",
       "      <td>INA</td>\n",
       "      <td>False</td>\n",
       "    </tr>\n",
       "    <tr>\n",
       "      <th>1047</th>\n",
       "      <td>JNA</td>\n",
       "      <td>False</td>\n",
       "    </tr>\n",
       "    <tr>\n",
       "      <th>1048</th>\n",
       "      <td>KNA</td>\n",
       "      <td>False</td>\n",
       "    </tr>\n",
       "    <tr>\n",
       "      <th>1049</th>\n",
       "      <td>LNA</td>\n",
       "      <td>False</td>\n",
       "    </tr>\n",
       "  </tbody>\n",
       "</table>\n",
       "<p>1050 rows × 2 columns</p>\n",
       "</div>"
      ]
     },
     "execution_count": 24,
     "metadata": {},
     "output_type": "execute_result"
    }
   ],
   "execution_count": 24
  },
  {
   "cell_type": "markdown",
   "metadata": {},
   "source": [
    "### `p_does_a_and_eventually_b`"
   ]
  },
  {
   "cell_type": "code",
   "metadata": {
    "ExecuteTime": {
     "end_time": "2026-05-29T14:00:36.369652800Z",
     "start_time": "2026-05-29T14:00:33.876017900Z"
    }
   },
   "source": [
    "template: LTLTemplate = LTLTemplate('p_does_a_and_eventually_b')\n",
    "model : LTLModel = template.fill_template(['A', 'ER Registration', 'Leucocytes'], attr_type=['org:group', 'concept:name'])\n",
    "print(f\"Formula: {model.formula}\")\n",
    "analyzer = LTLAnalyzer(event_log, model)\n",
    "conf_check_res_df = analyzer.run()\n",
    "conf_check_res_df"
   ],
   "outputs": [
    {
     "name": "stdout",
     "output_type": "stream",
     "text": [
      "Formula: F((F(org_a  && con_erregistration)  && F(F(org_a  && con_leucocytes))))\n"
     ]
    },
    {
     "data": {
      "text/plain": [
       "     case:concept:name  accepted\n",
       "0                    A     False\n",
       "1                    B     False\n",
       "2                    C     False\n",
       "3                    D     False\n",
       "4                    E     False\n",
       "...                ...       ...\n",
       "1045               HNA     False\n",
       "1046               INA     False\n",
       "1047               JNA     False\n",
       "1048               KNA     False\n",
       "1049               LNA     False\n",
       "\n",
       "[1050 rows x 2 columns]"
      ],
      "text/html": [
       "<div>\n",
       "<style scoped>\n",
       "    .dataframe tbody tr th:only-of-type {\n",
       "        vertical-align: middle;\n",
       "    }\n",
       "\n",
       "    .dataframe tbody tr th {\n",
       "        vertical-align: top;\n",
       "    }\n",
       "\n",
       "    .dataframe thead th {\n",
       "        text-align: right;\n",
       "    }\n",
       "</style>\n",
       "<table border=\"1\" class=\"dataframe\">\n",
       "  <thead>\n",
       "    <tr style=\"text-align: right;\">\n",
       "      <th></th>\n",
       "      <th>case:concept:name</th>\n",
       "      <th>accepted</th>\n",
       "    </tr>\n",
       "  </thead>\n",
       "  <tbody>\n",
       "    <tr>\n",
       "      <th>0</th>\n",
       "      <td>A</td>\n",
       "      <td>False</td>\n",
       "    </tr>\n",
       "    <tr>\n",
       "      <th>1</th>\n",
       "      <td>B</td>\n",
       "      <td>False</td>\n",
       "    </tr>\n",
       "    <tr>\n",
       "      <th>2</th>\n",
       "      <td>C</td>\n",
       "      <td>False</td>\n",
       "    </tr>\n",
       "    <tr>\n",
       "      <th>3</th>\n",
       "      <td>D</td>\n",
       "      <td>False</td>\n",
       "    </tr>\n",
       "    <tr>\n",
       "      <th>4</th>\n",
       "      <td>E</td>\n",
       "      <td>False</td>\n",
       "    </tr>\n",
       "    <tr>\n",
       "      <th>...</th>\n",
       "      <td>...</td>\n",
       "      <td>...</td>\n",
       "    </tr>\n",
       "    <tr>\n",
       "      <th>1045</th>\n",
       "      <td>HNA</td>\n",
       "      <td>False</td>\n",
       "    </tr>\n",
       "    <tr>\n",
       "      <th>1046</th>\n",
       "      <td>INA</td>\n",
       "      <td>False</td>\n",
       "    </tr>\n",
       "    <tr>\n",
       "      <th>1047</th>\n",
       "      <td>JNA</td>\n",
       "      <td>False</td>\n",
       "    </tr>\n",
       "    <tr>\n",
       "      <th>1048</th>\n",
       "      <td>KNA</td>\n",
       "      <td>False</td>\n",
       "    </tr>\n",
       "    <tr>\n",
       "      <th>1049</th>\n",
       "      <td>LNA</td>\n",
       "      <td>False</td>\n",
       "    </tr>\n",
       "  </tbody>\n",
       "</table>\n",
       "<p>1050 rows × 2 columns</p>\n",
       "</div>"
      ]
     },
     "execution_count": 25,
     "metadata": {},
     "output_type": "execute_result"
    }
   ],
   "execution_count": 25
  },
  {
   "cell_type": "markdown",
   "metadata": {},
   "source": [
    "### `p_does_a_a_not_b`"
   ]
  },
  {
   "cell_type": "code",
   "metadata": {
    "ExecuteTime": {
     "end_time": "2026-05-29T14:00:37.190767900Z",
     "start_time": "2026-05-29T14:00:36.420165Z"
    }
   },
   "source": [
    "template: LTLTemplate = LTLTemplate('p_does_a_a_not_b')\n",
    "model : LTLModel = template.fill_template(['A', 'ER Registration', 'Leucocytes'], attr_type=['org:group', 'concept:name'])\n",
    "print(f\"Formula: {model.formula}\")\n",
    "analyzer = LTLAnalyzer(event_log, model)\n",
    "conf_check_res_df = analyzer.run()\n",
    "conf_check_res_df"
   ],
   "outputs": [
    {
     "name": "stdout",
     "output_type": "stream",
     "text": [
      "Formula: F((con_erregistration  &&  (!con_leucocytes  && org_a)))\n"
     ]
    },
    {
     "data": {
      "text/plain": [
       "     case:concept:name  accepted\n",
       "0                    A      True\n",
       "1                    B      True\n",
       "2                    C      True\n",
       "3                    D      True\n",
       "4                    E      True\n",
       "...                ...       ...\n",
       "1045               HNA      True\n",
       "1046               INA      True\n",
       "1047               JNA      True\n",
       "1048               KNA      True\n",
       "1049               LNA     False\n",
       "\n",
       "[1050 rows x 2 columns]"
      ],
      "text/html": [
       "<div>\n",
       "<style scoped>\n",
       "    .dataframe tbody tr th:only-of-type {\n",
       "        vertical-align: middle;\n",
       "    }\n",
       "\n",
       "    .dataframe tbody tr th {\n",
       "        vertical-align: top;\n",
       "    }\n",
       "\n",
       "    .dataframe thead th {\n",
       "        text-align: right;\n",
       "    }\n",
       "</style>\n",
       "<table border=\"1\" class=\"dataframe\">\n",
       "  <thead>\n",
       "    <tr style=\"text-align: right;\">\n",
       "      <th></th>\n",
       "      <th>case:concept:name</th>\n",
       "      <th>accepted</th>\n",
       "    </tr>\n",
       "  </thead>\n",
       "  <tbody>\n",
       "    <tr>\n",
       "      <th>0</th>\n",
       "      <td>A</td>\n",
       "      <td>True</td>\n",
       "    </tr>\n",
       "    <tr>\n",
       "      <th>1</th>\n",
       "      <td>B</td>\n",
       "      <td>True</td>\n",
       "    </tr>\n",
       "    <tr>\n",
       "      <th>2</th>\n",
       "      <td>C</td>\n",
       "      <td>True</td>\n",
       "    </tr>\n",
       "    <tr>\n",
       "      <th>3</th>\n",
       "      <td>D</td>\n",
       "      <td>True</td>\n",
       "    </tr>\n",
       "    <tr>\n",
       "      <th>4</th>\n",
       "      <td>E</td>\n",
       "      <td>True</td>\n",
       "    </tr>\n",
       "    <tr>\n",
       "      <th>...</th>\n",
       "      <td>...</td>\n",
       "      <td>...</td>\n",
       "    </tr>\n",
       "    <tr>\n",
       "      <th>1045</th>\n",
       "      <td>HNA</td>\n",
       "      <td>True</td>\n",
       "    </tr>\n",
       "    <tr>\n",
       "      <th>1046</th>\n",
       "      <td>INA</td>\n",
       "      <td>True</td>\n",
       "    </tr>\n",
       "    <tr>\n",
       "      <th>1047</th>\n",
       "      <td>JNA</td>\n",
       "      <td>True</td>\n",
       "    </tr>\n",
       "    <tr>\n",
       "      <th>1048</th>\n",
       "      <td>KNA</td>\n",
       "      <td>True</td>\n",
       "    </tr>\n",
       "    <tr>\n",
       "      <th>1049</th>\n",
       "      <td>LNA</td>\n",
       "      <td>False</td>\n",
       "    </tr>\n",
       "  </tbody>\n",
       "</table>\n",
       "<p>1050 rows × 2 columns</p>\n",
       "</div>"
      ]
     },
     "execution_count": 26,
     "metadata": {},
     "output_type": "execute_result"
    }
   ],
   "execution_count": 26
  },
  {
   "cell_type": "markdown",
   "metadata": {},
   "source": [
    "### `a_done_by_p_p_not_q`"
   ]
  },
  {
   "cell_type": "code",
   "metadata": {
    "ExecuteTime": {
     "end_time": "2026-05-29T14:00:38.962006Z",
     "start_time": "2026-05-29T14:00:38.310185100Z"
    }
   },
   "source": [
    "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: {model.formula}\")\n",
    "analyzer = LTLAnalyzer(event_log, model)\n",
    "conf_check_res_df = analyzer.run()\n",
    "conf_check_res_df"
   ],
   "outputs": [
    {
     "name": "stdout",
     "output_type": "stream",
     "text": [
      "Formula: F((org_a  &&   (!org_b  && con_erregistration)))\n"
     ]
    },
    {
     "data": {
      "text/plain": [
       "     case:concept:name  accepted\n",
       "0                    A      True\n",
       "1                    B      True\n",
       "2                    C      True\n",
       "3                    D      True\n",
       "4                    E      True\n",
       "...                ...       ...\n",
       "1045               HNA      True\n",
       "1046               INA      True\n",
       "1047               JNA      True\n",
       "1048               KNA      True\n",
       "1049               LNA     False\n",
       "\n",
       "[1050 rows x 2 columns]"
      ],
      "text/html": [
       "<div>\n",
       "<style scoped>\n",
       "    .dataframe tbody tr th:only-of-type {\n",
       "        vertical-align: middle;\n",
       "    }\n",
       "\n",
       "    .dataframe tbody tr th {\n",
       "        vertical-align: top;\n",
       "    }\n",
       "\n",
       "    .dataframe thead th {\n",
       "        text-align: right;\n",
       "    }\n",
       "</style>\n",
       "<table border=\"1\" class=\"dataframe\">\n",
       "  <thead>\n",
       "    <tr style=\"text-align: right;\">\n",
       "      <th></th>\n",
       "      <th>case:concept:name</th>\n",
       "      <th>accepted</th>\n",
       "    </tr>\n",
       "  </thead>\n",
       "  <tbody>\n",
       "    <tr>\n",
       "      <th>0</th>\n",
       "      <td>A</td>\n",
       "      <td>True</td>\n",
       "    </tr>\n",
       "    <tr>\n",
       "      <th>1</th>\n",
       "      <td>B</td>\n",
       "      <td>True</td>\n",
       "    </tr>\n",
       "    <tr>\n",
       "      <th>2</th>\n",
       "      <td>C</td>\n",
       "      <td>True</td>\n",
       "    </tr>\n",
       "    <tr>\n",
       "      <th>3</th>\n",
       "      <td>D</td>\n",
       "      <td>True</td>\n",
       "    </tr>\n",
       "    <tr>\n",
       "      <th>4</th>\n",
       "      <td>E</td>\n",
       "      <td>True</td>\n",
       "    </tr>\n",
       "    <tr>\n",
       "      <th>...</th>\n",
       "      <td>...</td>\n",
       "      <td>...</td>\n",
       "    </tr>\n",
       "    <tr>\n",
       "      <th>1045</th>\n",
       "      <td>HNA</td>\n",
       "      <td>True</td>\n",
       "    </tr>\n",
       "    <tr>\n",
       "      <th>1046</th>\n",
       "      <td>INA</td>\n",
       "      <td>True</td>\n",
       "    </tr>\n",
       "    <tr>\n",
       "      <th>1047</th>\n",
       "      <td>JNA</td>\n",
       "      <td>True</td>\n",
       "    </tr>\n",
       "    <tr>\n",
       "      <th>1048</th>\n",
       "      <td>KNA</td>\n",
       "      <td>True</td>\n",
       "    </tr>\n",
       "    <tr>\n",
       "      <th>1049</th>\n",
       "      <td>LNA</td>\n",
       "      <td>False</td>\n",
       "    </tr>\n",
       "  </tbody>\n",
       "</table>\n",
       "<p>1050 rows × 2 columns</p>\n",
       "</div>"
      ]
     },
     "execution_count": 27,
     "metadata": {},
     "output_type": "execute_result"
    }
   ],
   "execution_count": 27
  },
  {
   "cell_type": "markdown",
   "metadata": {},
   "source": [
    "## Conformance Checking with Target-Branched DECLARE templates\n",
    "\n",
    "For these binary templates, the `fill_template` method takes two lists of activities (in string format) as parameters. For each template, the instantiated template formula and its corresponding checking in the input log will be computed."
   ]
  },
  {
   "cell_type": "markdown",
   "metadata": {},
   "source": [
    "### `precedence`"
   ]
  },
  {
   "cell_type": "code",
   "metadata": {
    "ExecuteTime": {
     "end_time": "2026-05-29T14:00:39.911075500Z",
     "start_time": "2026-05-29T14:00:39.012652700Z"
    }
   },
   "source": [
    "template = LTLTemplate('precedence')\n",
    "activities_a = [\"ER Triage\", \"CRP\"]\n",
    "activities_b = [\"Leucocytes\", \"Admission NC\", \"Release A\"]\n",
    "model = template.fill_template(activities_a, activities_b)\n",
    "print(f\"Formula: {model.formula}\")\n",
    "analyzer = LTLAnalyzer(event_log, model)\n",
    "conf_check_res_df = analyzer.run()\n",
    "conf_check_res_df"
   ],
   "outputs": [
    {
     "name": "stdout",
     "output_type": "stream",
     "text": [
      "Formula: ((!(con_leucocytes || con_admissionnc || con_releasea))U(con_ertriage || con_crp)) || G(!(con_leucocytes || con_admissionnc || con_releasea))\n"
     ]
    },
    {
     "data": {
      "text/plain": [
       "     case:concept:name  accepted\n",
       "0                    A     False\n",
       "1                    B      True\n",
       "2                    C      True\n",
       "3                    D      True\n",
       "4                    E      True\n",
       "...                ...       ...\n",
       "1045               HNA      True\n",
       "1046               INA      True\n",
       "1047               JNA      True\n",
       "1048               KNA      True\n",
       "1049               LNA      True\n",
       "\n",
       "[1050 rows x 2 columns]"
      ],
      "text/html": [
       "<div>\n",
       "<style scoped>\n",
       "    .dataframe tbody tr th:only-of-type {\n",
       "        vertical-align: middle;\n",
       "    }\n",
       "\n",
       "    .dataframe tbody tr th {\n",
       "        vertical-align: top;\n",
       "    }\n",
       "\n",
       "    .dataframe thead th {\n",
       "        text-align: right;\n",
       "    }\n",
       "</style>\n",
       "<table border=\"1\" class=\"dataframe\">\n",
       "  <thead>\n",
       "    <tr style=\"text-align: right;\">\n",
       "      <th></th>\n",
       "      <th>case:concept:name</th>\n",
       "      <th>accepted</th>\n",
       "    </tr>\n",
       "  </thead>\n",
       "  <tbody>\n",
       "    <tr>\n",
       "      <th>0</th>\n",
       "      <td>A</td>\n",
       "      <td>False</td>\n",
       "    </tr>\n",
       "    <tr>\n",
       "      <th>1</th>\n",
       "      <td>B</td>\n",
       "      <td>True</td>\n",
       "    </tr>\n",
       "    <tr>\n",
       "      <th>2</th>\n",
       "      <td>C</td>\n",
       "      <td>True</td>\n",
       "    </tr>\n",
       "    <tr>\n",
       "      <th>3</th>\n",
       "      <td>D</td>\n",
       "      <td>True</td>\n",
       "    </tr>\n",
       "    <tr>\n",
       "      <th>4</th>\n",
       "      <td>E</td>\n",
       "      <td>True</td>\n",
       "    </tr>\n",
       "    <tr>\n",
       "      <th>...</th>\n",
       "      <td>...</td>\n",
       "      <td>...</td>\n",
       "    </tr>\n",
       "    <tr>\n",
       "      <th>1045</th>\n",
       "      <td>HNA</td>\n",
       "      <td>True</td>\n",
       "    </tr>\n",
       "    <tr>\n",
       "      <th>1046</th>\n",
       "      <td>INA</td>\n",
       "      <td>True</td>\n",
       "    </tr>\n",
       "    <tr>\n",
       "      <th>1047</th>\n",
       "      <td>JNA</td>\n",
       "      <td>True</td>\n",
       "    </tr>\n",
       "    <tr>\n",
       "      <th>1048</th>\n",
       "      <td>KNA</td>\n",
       "      <td>True</td>\n",
       "    </tr>\n",
       "    <tr>\n",
       "      <th>1049</th>\n",
       "      <td>LNA</td>\n",
       "      <td>True</td>\n",
       "    </tr>\n",
       "  </tbody>\n",
       "</table>\n",
       "<p>1050 rows × 2 columns</p>\n",
       "</div>"
      ]
     },
     "execution_count": 28,
     "metadata": {},
     "output_type": "execute_result"
    }
   ],
   "execution_count": 28
  },
  {
   "cell_type": "markdown",
   "metadata": {},
   "source": [
    "### `chain_precedence`"
   ]
  },
  {
   "cell_type": "code",
   "metadata": {
    "ExecuteTime": {
     "end_time": "2026-05-29T14:00:42.299973100Z",
     "start_time": "2026-05-29T14:00:40.871870800Z"
    }
   },
   "source": [
    "template = LTLTemplate('chain_precedence')\n",
    "activities_a = [\"ER Triage\", \"CRP\", \"Leucocytes\"]\n",
    "activities_b = [\"Leucocytes\", \"Admission NC\", \"Release A\"]\n",
    "model = template.fill_template(activities_a, activities_b)\n",
    "print(f\"Formula: {model.formula}\")\n",
    "analyzer = LTLAnalyzer(event_log, model)\n",
    "conf_check_res_df = analyzer.run()\n",
    "conf_check_res_df"
   ],
   "outputs": [
    {
     "name": "stdout",
     "output_type": "stream",
     "text": [
      "Formula: G(X[!](con_leucocytes || con_admissionnc || con_releasea) ->  (con_ertriage || con_crp || con_leucocytes))\n"
     ]
    },
    {
     "data": {
      "text/plain": [
       "     case:concept:name  accepted\n",
       "0                    A     False\n",
       "1                    B     False\n",
       "2                    C     False\n",
       "3                    D     False\n",
       "4                    E      True\n",
       "...                ...       ...\n",
       "1045               HNA     False\n",
       "1046               INA      True\n",
       "1047               JNA      True\n",
       "1048               KNA     False\n",
       "1049               LNA      True\n",
       "\n",
       "[1050 rows x 2 columns]"
      ],
      "text/html": [
       "<div>\n",
       "<style scoped>\n",
       "    .dataframe tbody tr th:only-of-type {\n",
       "        vertical-align: middle;\n",
       "    }\n",
       "\n",
       "    .dataframe tbody tr th {\n",
       "        vertical-align: top;\n",
       "    }\n",
       "\n",
       "    .dataframe thead th {\n",
       "        text-align: right;\n",
       "    }\n",
       "</style>\n",
       "<table border=\"1\" class=\"dataframe\">\n",
       "  <thead>\n",
       "    <tr style=\"text-align: right;\">\n",
       "      <th></th>\n",
       "      <th>case:concept:name</th>\n",
       "      <th>accepted</th>\n",
       "    </tr>\n",
       "  </thead>\n",
       "  <tbody>\n",
       "    <tr>\n",
       "      <th>0</th>\n",
       "      <td>A</td>\n",
       "      <td>False</td>\n",
       "    </tr>\n",
       "    <tr>\n",
       "      <th>1</th>\n",
       "      <td>B</td>\n",
       "      <td>False</td>\n",
       "    </tr>\n",
       "    <tr>\n",
       "      <th>2</th>\n",
       "      <td>C</td>\n",
       "      <td>False</td>\n",
       "    </tr>\n",
       "    <tr>\n",
       "      <th>3</th>\n",
       "      <td>D</td>\n",
       "      <td>False</td>\n",
       "    </tr>\n",
       "    <tr>\n",
       "      <th>4</th>\n",
       "      <td>E</td>\n",
       "      <td>True</td>\n",
       "    </tr>\n",
       "    <tr>\n",
       "      <th>...</th>\n",
       "      <td>...</td>\n",
       "      <td>...</td>\n",
       "    </tr>\n",
       "    <tr>\n",
       "      <th>1045</th>\n",
       "      <td>HNA</td>\n",
       "      <td>False</td>\n",
       "    </tr>\n",
       "    <tr>\n",
       "      <th>1046</th>\n",
       "      <td>INA</td>\n",
       "      <td>True</td>\n",
       "    </tr>\n",
       "    <tr>\n",
       "      <th>1047</th>\n",
       "      <td>JNA</td>\n",
       "      <td>True</td>\n",
       "    </tr>\n",
       "    <tr>\n",
       "      <th>1048</th>\n",
       "      <td>KNA</td>\n",
       "      <td>False</td>\n",
       "    </tr>\n",
       "    <tr>\n",
       "      <th>1049</th>\n",
       "      <td>LNA</td>\n",
       "      <td>True</td>\n",
       "    </tr>\n",
       "  </tbody>\n",
       "</table>\n",
       "<p>1050 rows × 2 columns</p>\n",
       "</div>"
      ]
     },
     "execution_count": 29,
     "metadata": {},
     "output_type": "execute_result"
    }
   ],
   "execution_count": 29
  },
  {
   "cell_type": "markdown",
   "metadata": {},
   "source": [
    "### `responded_existence`"
   ]
  },
  {
   "cell_type": "code",
   "metadata": {
    "ExecuteTime": {
     "end_time": "2026-05-29T14:00:43.685253400Z",
     "start_time": "2026-05-29T14:00:42.353989400Z"
    }
   },
   "source": [
    "template = LTLTemplate('responded_existence')\n",
    "activities_a = [\"ER Triage\", \"CRP\", \"Leucocytes\"]\n",
    "activities_b = [\"Leucocytes\", \"Admission NC\", \"Release A\"]\n",
    "model = template.fill_template(activities_a, activities_b)\n",
    "print(f\"Formula: {model.formula}\")\n",
    "analyzer = LTLAnalyzer(event_log, model)\n",
    "conf_check_res_df = analyzer.run()\n",
    "conf_check_res_df"
   ],
   "outputs": [
    {
     "name": "stdout",
     "output_type": "stream",
     "text": [
      "Formula: F(con_ertriage || con_crp || con_leucocytes) -> F(con_leucocytes || con_admissionnc || con_releasea)\n"
     ]
    },
    {
     "data": {
      "text/plain": [
       "     case:concept:name  accepted\n",
       "0                    A      True\n",
       "1                    B      True\n",
       "2                    C      True\n",
       "3                    D      True\n",
       "4                    E      True\n",
       "...                ...       ...\n",
       "1045               HNA      True\n",
       "1046               INA     False\n",
       "1047               JNA     False\n",
       "1048               KNA      True\n",
       "1049               LNA     False\n",
       "\n",
       "[1050 rows x 2 columns]"
      ],
      "text/html": [
       "<div>\n",
       "<style scoped>\n",
       "    .dataframe tbody tr th:only-of-type {\n",
       "        vertical-align: middle;\n",
       "    }\n",
       "\n",
       "    .dataframe tbody tr th {\n",
       "        vertical-align: top;\n",
       "    }\n",
       "\n",
       "    .dataframe thead th {\n",
       "        text-align: right;\n",
       "    }\n",
       "</style>\n",
       "<table border=\"1\" class=\"dataframe\">\n",
       "  <thead>\n",
       "    <tr style=\"text-align: right;\">\n",
       "      <th></th>\n",
       "      <th>case:concept:name</th>\n",
       "      <th>accepted</th>\n",
       "    </tr>\n",
       "  </thead>\n",
       "  <tbody>\n",
       "    <tr>\n",
       "      <th>0</th>\n",
       "      <td>A</td>\n",
       "      <td>True</td>\n",
       "    </tr>\n",
       "    <tr>\n",
       "      <th>1</th>\n",
       "      <td>B</td>\n",
       "      <td>True</td>\n",
       "    </tr>\n",
       "    <tr>\n",
       "      <th>2</th>\n",
       "      <td>C</td>\n",
       "      <td>True</td>\n",
       "    </tr>\n",
       "    <tr>\n",
       "      <th>3</th>\n",
       "      <td>D</td>\n",
       "      <td>True</td>\n",
       "    </tr>\n",
       "    <tr>\n",
       "      <th>4</th>\n",
       "      <td>E</td>\n",
       "      <td>True</td>\n",
       "    </tr>\n",
       "    <tr>\n",
       "      <th>...</th>\n",
       "      <td>...</td>\n",
       "      <td>...</td>\n",
       "    </tr>\n",
       "    <tr>\n",
       "      <th>1045</th>\n",
       "      <td>HNA</td>\n",
       "      <td>True</td>\n",
       "    </tr>\n",
       "    <tr>\n",
       "      <th>1046</th>\n",
       "      <td>INA</td>\n",
       "      <td>False</td>\n",
       "    </tr>\n",
       "    <tr>\n",
       "      <th>1047</th>\n",
       "      <td>JNA</td>\n",
       "      <td>False</td>\n",
       "    </tr>\n",
       "    <tr>\n",
       "      <th>1048</th>\n",
       "      <td>KNA</td>\n",
       "      <td>True</td>\n",
       "    </tr>\n",
       "    <tr>\n",
       "      <th>1049</th>\n",
       "      <td>LNA</td>\n",
       "      <td>False</td>\n",
       "    </tr>\n",
       "  </tbody>\n",
       "</table>\n",
       "<p>1050 rows × 2 columns</p>\n",
       "</div>"
      ]
     },
     "execution_count": 30,
     "metadata": {},
     "output_type": "execute_result"
    }
   ],
   "execution_count": 30
  },
  {
   "cell_type": "markdown",
   "metadata": {},
   "source": [
    "### `chain_response`"
   ]
  },
  {
   "cell_type": "code",
   "metadata": {
    "ExecuteTime": {
     "end_time": "2026-05-29T14:00:46.591447400Z",
     "start_time": "2026-05-29T14:00:44.770492300Z"
    }
   },
   "source": [
    "template = LTLTemplate('chain_response')\n",
    "activities_a = [\"ER Registration\", \"CRP\"]\n",
    "activities_b = [\"ER Triage\", \"Leucocytes\", \"Release A\"]\n",
    "model = template.fill_template(activities_a, activities_b)\n",
    "print(f\"Formula: {model.formula}\")\n",
    "analyzer = LTLAnalyzer(event_log, model)\n",
    "conf_check_res_df = analyzer.run()\n",
    "conf_check_res_df"
   ],
   "outputs": [
    {
     "name": "stdout",
     "output_type": "stream",
     "text": [
      "Formula: G((con_erregistration  || con_crp) -> X[!](con_ertriage || con_leucocytes || con_releasea))\n"
     ]
    },
    {
     "data": {
      "text/plain": [
       "     case:concept:name  accepted\n",
       "0                    A     False\n",
       "1                    B     False\n",
       "2                    C     False\n",
       "3                    D     False\n",
       "4                    E      True\n",
       "...                ...       ...\n",
       "1045               HNA     False\n",
       "1046               INA      True\n",
       "1047               JNA      True\n",
       "1048               KNA     False\n",
       "1049               LNA      True\n",
       "\n",
       "[1050 rows x 2 columns]"
      ],
      "text/html": [
       "<div>\n",
       "<style scoped>\n",
       "    .dataframe tbody tr th:only-of-type {\n",
       "        vertical-align: middle;\n",
       "    }\n",
       "\n",
       "    .dataframe tbody tr th {\n",
       "        vertical-align: top;\n",
       "    }\n",
       "\n",
       "    .dataframe thead th {\n",
       "        text-align: right;\n",
       "    }\n",
       "</style>\n",
       "<table border=\"1\" class=\"dataframe\">\n",
       "  <thead>\n",
       "    <tr style=\"text-align: right;\">\n",
       "      <th></th>\n",
       "      <th>case:concept:name</th>\n",
       "      <th>accepted</th>\n",
       "    </tr>\n",
       "  </thead>\n",
       "  <tbody>\n",
       "    <tr>\n",
       "      <th>0</th>\n",
       "      <td>A</td>\n",
       "      <td>False</td>\n",
       "    </tr>\n",
       "    <tr>\n",
       "      <th>1</th>\n",
       "      <td>B</td>\n",
       "      <td>False</td>\n",
       "    </tr>\n",
       "    <tr>\n",
       "      <th>2</th>\n",
       "      <td>C</td>\n",
       "      <td>False</td>\n",
       "    </tr>\n",
       "    <tr>\n",
       "      <th>3</th>\n",
       "      <td>D</td>\n",
       "      <td>False</td>\n",
       "    </tr>\n",
       "    <tr>\n",
       "      <th>4</th>\n",
       "      <td>E</td>\n",
       "      <td>True</td>\n",
       "    </tr>\n",
       "    <tr>\n",
       "      <th>...</th>\n",
       "      <td>...</td>\n",
       "      <td>...</td>\n",
       "    </tr>\n",
       "    <tr>\n",
       "      <th>1045</th>\n",
       "      <td>HNA</td>\n",
       "      <td>False</td>\n",
       "    </tr>\n",
       "    <tr>\n",
       "      <th>1046</th>\n",
       "      <td>INA</td>\n",
       "      <td>True</td>\n",
       "    </tr>\n",
       "    <tr>\n",
       "      <th>1047</th>\n",
       "      <td>JNA</td>\n",
       "      <td>True</td>\n",
       "    </tr>\n",
       "    <tr>\n",
       "      <th>1048</th>\n",
       "      <td>KNA</td>\n",
       "      <td>False</td>\n",
       "    </tr>\n",
       "    <tr>\n",
       "      <th>1049</th>\n",
       "      <td>LNA</td>\n",
       "      <td>True</td>\n",
       "    </tr>\n",
       "  </tbody>\n",
       "</table>\n",
       "<p>1050 rows × 2 columns</p>\n",
       "</div>"
      ]
     },
     "execution_count": 31,
     "metadata": {},
     "output_type": "execute_result"
    }
   ],
   "execution_count": 31
  },
  {
   "cell_type": "markdown",
   "metadata": {},
   "source": [
    "### `not_chain_precedence`"
   ]
  },
  {
   "cell_type": "code",
   "metadata": {
    "ExecuteTime": {
     "end_time": "2026-05-29T14:00:48.379490700Z",
     "start_time": "2026-05-29T14:00:46.644962200Z"
    }
   },
   "source": [
    "template = LTLTemplate('not_chain_precedence')\n",
    "activities_a = [\"ER Triage\", \"CRP\", \"Leucocytes\"]\n",
    "activities_b = [\"Leucocytes\", \"Admission NC\", \"Release A\"]\n",
    "model = template.fill_template(activities_a, activities_b)\n",
    "print(f\"Formula: {model.formula}\")\n",
    "analyzer = LTLAnalyzer(event_log, model)\n",
    "conf_check_res_df = analyzer.run()\n",
    "conf_check_res_df"
   ],
   "outputs": [
    {
     "name": "stdout",
     "output_type": "stream",
     "text": [
      "Formula: G(X[!](con_leucocytes || con_admissionnc || con_releasea) ->  !(con_ertriage || con_crp || con_leucocytes))\n"
     ]
    },
    {
     "data": {
      "text/plain": [
       "     case:concept:name  accepted\n",
       "0                    A     False\n",
       "1                    B     False\n",
       "2                    C     False\n",
       "3                    D     False\n",
       "4                    E     False\n",
       "...                ...       ...\n",
       "1045               HNA     False\n",
       "1046               INA      True\n",
       "1047               JNA      True\n",
       "1048               KNA     False\n",
       "1049               LNA      True\n",
       "\n",
       "[1050 rows x 2 columns]"
      ],
      "text/html": [
       "<div>\n",
       "<style scoped>\n",
       "    .dataframe tbody tr th:only-of-type {\n",
       "        vertical-align: middle;\n",
       "    }\n",
       "\n",
       "    .dataframe tbody tr th {\n",
       "        vertical-align: top;\n",
       "    }\n",
       "\n",
       "    .dataframe thead th {\n",
       "        text-align: right;\n",
       "    }\n",
       "</style>\n",
       "<table border=\"1\" class=\"dataframe\">\n",
       "  <thead>\n",
       "    <tr style=\"text-align: right;\">\n",
       "      <th></th>\n",
       "      <th>case:concept:name</th>\n",
       "      <th>accepted</th>\n",
       "    </tr>\n",
       "  </thead>\n",
       "  <tbody>\n",
       "    <tr>\n",
       "      <th>0</th>\n",
       "      <td>A</td>\n",
       "      <td>False</td>\n",
       "    </tr>\n",
       "    <tr>\n",
       "      <th>1</th>\n",
       "      <td>B</td>\n",
       "      <td>False</td>\n",
       "    </tr>\n",
       "    <tr>\n",
       "      <th>2</th>\n",
       "      <td>C</td>\n",
       "      <td>False</td>\n",
       "    </tr>\n",
       "    <tr>\n",
       "      <th>3</th>\n",
       "      <td>D</td>\n",
       "      <td>False</td>\n",
       "    </tr>\n",
       "    <tr>\n",
       "      <th>4</th>\n",
       "      <td>E</td>\n",
       "      <td>False</td>\n",
       "    </tr>\n",
       "    <tr>\n",
       "      <th>...</th>\n",
       "      <td>...</td>\n",
       "      <td>...</td>\n",
       "    </tr>\n",
       "    <tr>\n",
       "      <th>1045</th>\n",
       "      <td>HNA</td>\n",
       "      <td>False</td>\n",
       "    </tr>\n",
       "    <tr>\n",
       "      <th>1046</th>\n",
       "      <td>INA</td>\n",
       "      <td>True</td>\n",
       "    </tr>\n",
       "    <tr>\n",
       "      <th>1047</th>\n",
       "      <td>JNA</td>\n",
       "      <td>True</td>\n",
       "    </tr>\n",
       "    <tr>\n",
       "      <th>1048</th>\n",
       "      <td>KNA</td>\n",
       "      <td>False</td>\n",
       "    </tr>\n",
       "    <tr>\n",
       "      <th>1049</th>\n",
       "      <td>LNA</td>\n",
       "      <td>True</td>\n",
       "    </tr>\n",
       "  </tbody>\n",
       "</table>\n",
       "<p>1050 rows × 2 columns</p>\n",
       "</div>"
      ]
     },
     "execution_count": 32,
     "metadata": {},
     "output_type": "execute_result"
    }
   ],
   "execution_count": 32
  },
  {
   "cell_type": "markdown",
   "metadata": {},
   "source": [
    "### `not_chain_response`"
   ]
  },
  {
   "cell_type": "code",
   "metadata": {
    "ExecuteTime": {
     "end_time": "2026-05-29T14:00:51.082728700Z",
     "start_time": "2026-05-29T14:00:49.404822600Z"
    }
   },
   "source": [
    "template = LTLTemplate('not_chain_response')\n",
    "activities_a = [\"ER Triage\", \"CRP\", \"Leucocytes\"]\n",
    "activities_b = [\"Leucocytes\", \"Admission NC\", \"Release A\"]\n",
    "model = template.fill_template(activities_a, activities_b)\n",
    "print(f\"Formula: {model.formula}\")\n",
    "analyzer = LTLAnalyzer(event_log, model)\n",
    "conf_check_res_df = analyzer.run()\n",
    "conf_check_res_df"
   ],
   "outputs": [
    {
     "name": "stdout",
     "output_type": "stream",
     "text": [
      "Formula: G((con_ertriage || con_crp || con_leucocytes) -> X[!](!(con_leucocytes || con_admissionnc || con_releasea)))\n"
     ]
    },
    {
     "data": {
      "text/plain": [
       "     case:concept:name  accepted\n",
       "0                    A     False\n",
       "1                    B     False\n",
       "2                    C     False\n",
       "3                    D     False\n",
       "4                    E     False\n",
       "...                ...       ...\n",
       "1045               HNA     False\n",
       "1046               INA      True\n",
       "1047               JNA      True\n",
       "1048               KNA     False\n",
       "1049               LNA      True\n",
       "\n",
       "[1050 rows x 2 columns]"
      ],
      "text/html": [
       "<div>\n",
       "<style scoped>\n",
       "    .dataframe tbody tr th:only-of-type {\n",
       "        vertical-align: middle;\n",
       "    }\n",
       "\n",
       "    .dataframe tbody tr th {\n",
       "        vertical-align: top;\n",
       "    }\n",
       "\n",
       "    .dataframe thead th {\n",
       "        text-align: right;\n",
       "    }\n",
       "</style>\n",
       "<table border=\"1\" class=\"dataframe\">\n",
       "  <thead>\n",
       "    <tr style=\"text-align: right;\">\n",
       "      <th></th>\n",
       "      <th>case:concept:name</th>\n",
       "      <th>accepted</th>\n",
       "    </tr>\n",
       "  </thead>\n",
       "  <tbody>\n",
       "    <tr>\n",
       "      <th>0</th>\n",
       "      <td>A</td>\n",
       "      <td>False</td>\n",
       "    </tr>\n",
       "    <tr>\n",
       "      <th>1</th>\n",
       "      <td>B</td>\n",
       "      <td>False</td>\n",
       "    </tr>\n",
       "    <tr>\n",
       "      <th>2</th>\n",
       "      <td>C</td>\n",
       "      <td>False</td>\n",
       "    </tr>\n",
       "    <tr>\n",
       "      <th>3</th>\n",
       "      <td>D</td>\n",
       "      <td>False</td>\n",
       "    </tr>\n",
       "    <tr>\n",
       "      <th>4</th>\n",
       "      <td>E</td>\n",
       "      <td>False</td>\n",
       "    </tr>\n",
       "    <tr>\n",
       "      <th>...</th>\n",
       "      <td>...</td>\n",
       "      <td>...</td>\n",
       "    </tr>\n",
       "    <tr>\n",
       "      <th>1045</th>\n",
       "      <td>HNA</td>\n",
       "      <td>False</td>\n",
       "    </tr>\n",
       "    <tr>\n",
       "      <th>1046</th>\n",
       "      <td>INA</td>\n",
       "      <td>True</td>\n",
       "    </tr>\n",
       "    <tr>\n",
       "      <th>1047</th>\n",
       "      <td>JNA</td>\n",
       "      <td>True</td>\n",
       "    </tr>\n",
       "    <tr>\n",
       "      <th>1048</th>\n",
       "      <td>KNA</td>\n",
       "      <td>False</td>\n",
       "    </tr>\n",
       "    <tr>\n",
       "      <th>1049</th>\n",
       "      <td>LNA</td>\n",
       "      <td>True</td>\n",
       "    </tr>\n",
       "  </tbody>\n",
       "</table>\n",
       "<p>1050 rows × 2 columns</p>\n",
       "</div>"
      ]
     },
     "execution_count": 33,
     "metadata": {},
     "output_type": "execute_result"
    }
   ],
   "execution_count": 33
  },
  {
   "cell_type": "markdown",
   "metadata": {},
   "source": [
    "### `response`"
   ]
  },
  {
   "cell_type": "code",
   "metadata": {
    "ExecuteTime": {
     "end_time": "2026-05-29T14:00:53.412833600Z",
     "start_time": "2026-05-29T14:00:51.136107200Z"
    }
   },
   "source": [
    "template = LTLTemplate('response')\n",
    "activities_a = [\"ER Triage\", \"CRP\", \"Leucocytes\"]\n",
    "activities_b = [\"Leucocytes\", \"Admission NC\", \"Release A\"]\n",
    "model = template.fill_template(activities_a, activities_b)\n",
    "print(f\"Formula: {model.formula}\")\n",
    "analyzer = LTLAnalyzer(event_log, model)\n",
    "conf_check_res_df = analyzer.run()\n",
    "conf_check_res_df"
   ],
   "outputs": [
    {
     "name": "stdout",
     "output_type": "stream",
     "text": [
      "Formula: G((con_ertriage || con_crp || con_leucocytes) -> F(con_leucocytes || con_admissionnc || con_releasea))\n"
     ]
    },
    {
     "data": {
      "text/plain": [
       "     case:concept:name  accepted\n",
       "0                    A      True\n",
       "1                    B      True\n",
       "2                    C      True\n",
       "3                    D      True\n",
       "4                    E      True\n",
       "...                ...       ...\n",
       "1045               HNA      True\n",
       "1046               INA     False\n",
       "1047               JNA     False\n",
       "1048               KNA      True\n",
       "1049               LNA     False\n",
       "\n",
       "[1050 rows x 2 columns]"
      ],
      "text/html": [
       "<div>\n",
       "<style scoped>\n",
       "    .dataframe tbody tr th:only-of-type {\n",
       "        vertical-align: middle;\n",
       "    }\n",
       "\n",
       "    .dataframe tbody tr th {\n",
       "        vertical-align: top;\n",
       "    }\n",
       "\n",
       "    .dataframe thead th {\n",
       "        text-align: right;\n",
       "    }\n",
       "</style>\n",
       "<table border=\"1\" class=\"dataframe\">\n",
       "  <thead>\n",
       "    <tr style=\"text-align: right;\">\n",
       "      <th></th>\n",
       "      <th>case:concept:name</th>\n",
       "      <th>accepted</th>\n",
       "    </tr>\n",
       "  </thead>\n",
       "  <tbody>\n",
       "    <tr>\n",
       "      <th>0</th>\n",
       "      <td>A</td>\n",
       "      <td>True</td>\n",
       "    </tr>\n",
       "    <tr>\n",
       "      <th>1</th>\n",
       "      <td>B</td>\n",
       "      <td>True</td>\n",
       "    </tr>\n",
       "    <tr>\n",
       "      <th>2</th>\n",
       "      <td>C</td>\n",
       "      <td>True</td>\n",
       "    </tr>\n",
       "    <tr>\n",
       "      <th>3</th>\n",
       "      <td>D</td>\n",
       "      <td>True</td>\n",
       "    </tr>\n",
       "    <tr>\n",
       "      <th>4</th>\n",
       "      <td>E</td>\n",
       "      <td>True</td>\n",
       "    </tr>\n",
       "    <tr>\n",
       "      <th>...</th>\n",
       "      <td>...</td>\n",
       "      <td>...</td>\n",
       "    </tr>\n",
       "    <tr>\n",
       "      <th>1045</th>\n",
       "      <td>HNA</td>\n",
       "      <td>True</td>\n",
       "    </tr>\n",
       "    <tr>\n",
       "      <th>1046</th>\n",
       "      <td>INA</td>\n",
       "      <td>False</td>\n",
       "    </tr>\n",
       "    <tr>\n",
       "      <th>1047</th>\n",
       "      <td>JNA</td>\n",
       "      <td>False</td>\n",
       "    </tr>\n",
       "    <tr>\n",
       "      <th>1048</th>\n",
       "      <td>KNA</td>\n",
       "      <td>True</td>\n",
       "    </tr>\n",
       "    <tr>\n",
       "      <th>1049</th>\n",
       "      <td>LNA</td>\n",
       "      <td>False</td>\n",
       "    </tr>\n",
       "  </tbody>\n",
       "</table>\n",
       "<p>1050 rows × 2 columns</p>\n",
       "</div>"
      ]
     },
     "execution_count": 34,
     "metadata": {},
     "output_type": "execute_result"
    }
   ],
   "execution_count": 34
  },
  {
   "cell_type": "markdown",
   "metadata": {},
   "source": [
    "### `not_precedence`"
   ]
  },
  {
   "cell_type": "code",
   "metadata": {
    "ExecuteTime": {
     "end_time": "2026-05-29T14:00:55.880409100Z",
     "start_time": "2026-05-29T14:00:54.369933Z"
    }
   },
   "source": [
    "template = LTLTemplate('not_precedence')\n",
    "activities_a = [\"ER Triage\", \"CRP\", \"Leucocytes\"]\n",
    "activities_b = [\"Leucocytes\", \"Admission NC\", \"Release A\"]\n",
    "model = template.fill_template(activities_a, activities_b)\n",
    "print(f\"Formula: {model.formula}\")\n",
    "analyzer = LTLAnalyzer(event_log, model)\n",
    "conf_check_res_df = analyzer.run()\n",
    "conf_check_res_df"
   ],
   "outputs": [
    {
     "name": "stdout",
     "output_type": "stream",
     "text": [
      "Formula: G(F(con_leucocytes || con_admissionnc || con_releasea) -> !(con_ertriage || con_crp || con_leucocytes))\n"
     ]
    },
    {
     "data": {
      "text/plain": [
       "     case:concept:name  accepted\n",
       "0                    A     False\n",
       "1                    B     False\n",
       "2                    C     False\n",
       "3                    D     False\n",
       "4                    E     False\n",
       "...                ...       ...\n",
       "1045               HNA     False\n",
       "1046               INA      True\n",
       "1047               JNA      True\n",
       "1048               KNA     False\n",
       "1049               LNA      True\n",
       "\n",
       "[1050 rows x 2 columns]"
      ],
      "text/html": [
       "<div>\n",
       "<style scoped>\n",
       "    .dataframe tbody tr th:only-of-type {\n",
       "        vertical-align: middle;\n",
       "    }\n",
       "\n",
       "    .dataframe tbody tr th {\n",
       "        vertical-align: top;\n",
       "    }\n",
       "\n",
       "    .dataframe thead th {\n",
       "        text-align: right;\n",
       "    }\n",
       "</style>\n",
       "<table border=\"1\" class=\"dataframe\">\n",
       "  <thead>\n",
       "    <tr style=\"text-align: right;\">\n",
       "      <th></th>\n",
       "      <th>case:concept:name</th>\n",
       "      <th>accepted</th>\n",
       "    </tr>\n",
       "  </thead>\n",
       "  <tbody>\n",
       "    <tr>\n",
       "      <th>0</th>\n",
       "      <td>A</td>\n",
       "      <td>False</td>\n",
       "    </tr>\n",
       "    <tr>\n",
       "      <th>1</th>\n",
       "      <td>B</td>\n",
       "      <td>False</td>\n",
       "    </tr>\n",
       "    <tr>\n",
       "      <th>2</th>\n",
       "      <td>C</td>\n",
       "      <td>False</td>\n",
       "    </tr>\n",
       "    <tr>\n",
       "      <th>3</th>\n",
       "      <td>D</td>\n",
       "      <td>False</td>\n",
       "    </tr>\n",
       "    <tr>\n",
       "      <th>4</th>\n",
       "      <td>E</td>\n",
       "      <td>False</td>\n",
       "    </tr>\n",
       "    <tr>\n",
       "      <th>...</th>\n",
       "      <td>...</td>\n",
       "      <td>...</td>\n",
       "    </tr>\n",
       "    <tr>\n",
       "      <th>1045</th>\n",
       "      <td>HNA</td>\n",
       "      <td>False</td>\n",
       "    </tr>\n",
       "    <tr>\n",
       "      <th>1046</th>\n",
       "      <td>INA</td>\n",
       "      <td>True</td>\n",
       "    </tr>\n",
       "    <tr>\n",
       "      <th>1047</th>\n",
       "      <td>JNA</td>\n",
       "      <td>True</td>\n",
       "    </tr>\n",
       "    <tr>\n",
       "      <th>1048</th>\n",
       "      <td>KNA</td>\n",
       "      <td>False</td>\n",
       "    </tr>\n",
       "    <tr>\n",
       "      <th>1049</th>\n",
       "      <td>LNA</td>\n",
       "      <td>True</td>\n",
       "    </tr>\n",
       "  </tbody>\n",
       "</table>\n",
       "<p>1050 rows × 2 columns</p>\n",
       "</div>"
      ]
     },
     "execution_count": 35,
     "metadata": {},
     "output_type": "execute_result"
    }
   ],
   "execution_count": 35
  },
  {
   "cell_type": "markdown",
   "metadata": {},
   "source": [
    "### `not_response`"
   ]
  },
  {
   "cell_type": "code",
   "metadata": {
    "ExecuteTime": {
     "end_time": "2026-05-29T14:00:57.496600200Z",
     "start_time": "2026-05-29T14:00:55.948563500Z"
    }
   },
   "source": [
    "template = LTLTemplate('not_response')\n",
    "activities_a = [\"ER Triage\", \"CRP\", \"Leucocytes\"]\n",
    "activities_b = [\"Leucocytes\", \"Admission NC\", \"Release A\"]\n",
    "model = template.fill_template(activities_a, activities_b)\n",
    "print(f\"Formula: {model.formula}\")\n",
    "analyzer = LTLAnalyzer(event_log, model)\n",
    "conf_check_res_df = analyzer.run()\n",
    "conf_check_res_df"
   ],
   "outputs": [
    {
     "name": "stdout",
     "output_type": "stream",
     "text": [
      "Formula: G((con_ertriage || con_crp || con_leucocytes) ->  !(F(con_leucocytes || con_admissionnc || con_releasea)))\n"
     ]
    },
    {
     "data": {
      "text/plain": [
       "     case:concept:name  accepted\n",
       "0                    A     False\n",
       "1                    B     False\n",
       "2                    C     False\n",
       "3                    D     False\n",
       "4                    E     False\n",
       "...                ...       ...\n",
       "1045               HNA     False\n",
       "1046               INA      True\n",
       "1047               JNA      True\n",
       "1048               KNA     False\n",
       "1049               LNA      True\n",
       "\n",
       "[1050 rows x 2 columns]"
      ],
      "text/html": [
       "<div>\n",
       "<style scoped>\n",
       "    .dataframe tbody tr th:only-of-type {\n",
       "        vertical-align: middle;\n",
       "    }\n",
       "\n",
       "    .dataframe tbody tr th {\n",
       "        vertical-align: top;\n",
       "    }\n",
       "\n",
       "    .dataframe thead th {\n",
       "        text-align: right;\n",
       "    }\n",
       "</style>\n",
       "<table border=\"1\" class=\"dataframe\">\n",
       "  <thead>\n",
       "    <tr style=\"text-align: right;\">\n",
       "      <th></th>\n",
       "      <th>case:concept:name</th>\n",
       "      <th>accepted</th>\n",
       "    </tr>\n",
       "  </thead>\n",
       "  <tbody>\n",
       "    <tr>\n",
       "      <th>0</th>\n",
       "      <td>A</td>\n",
       "      <td>False</td>\n",
       "    </tr>\n",
       "    <tr>\n",
       "      <th>1</th>\n",
       "      <td>B</td>\n",
       "      <td>False</td>\n",
       "    </tr>\n",
       "    <tr>\n",
       "      <th>2</th>\n",
       "      <td>C</td>\n",
       "      <td>False</td>\n",
       "    </tr>\n",
       "    <tr>\n",
       "      <th>3</th>\n",
       "      <td>D</td>\n",
       "      <td>False</td>\n",
       "    </tr>\n",
       "    <tr>\n",
       "      <th>4</th>\n",
       "      <td>E</td>\n",
       "      <td>False</td>\n",
       "    </tr>\n",
       "    <tr>\n",
       "      <th>...</th>\n",
       "      <td>...</td>\n",
       "      <td>...</td>\n",
       "    </tr>\n",
       "    <tr>\n",
       "      <th>1045</th>\n",
       "      <td>HNA</td>\n",
       "      <td>False</td>\n",
       "    </tr>\n",
       "    <tr>\n",
       "      <th>1046</th>\n",
       "      <td>INA</td>\n",
       "      <td>True</td>\n",
       "    </tr>\n",
       "    <tr>\n",
       "      <th>1047</th>\n",
       "      <td>JNA</td>\n",
       "      <td>True</td>\n",
       "    </tr>\n",
       "    <tr>\n",
       "      <th>1048</th>\n",
       "      <td>KNA</td>\n",
       "      <td>False</td>\n",
       "    </tr>\n",
       "    <tr>\n",
       "      <th>1049</th>\n",
       "      <td>LNA</td>\n",
       "      <td>True</td>\n",
       "    </tr>\n",
       "  </tbody>\n",
       "</table>\n",
       "<p>1050 rows × 2 columns</p>\n",
       "</div>"
      ]
     },
     "execution_count": 36,
     "metadata": {},
     "output_type": "execute_result"
    }
   ],
   "execution_count": 36
  },
  {
   "cell_type": "markdown",
   "metadata": {},
   "source": [
    "### `not_responded_existence`"
   ]
  },
  {
   "cell_type": "code",
   "metadata": {
    "ExecuteTime": {
     "end_time": "2026-05-29T14:01:00.332394200Z",
     "start_time": "2026-05-29T14:00:58.565392200Z"
    }
   },
   "source": [
    "template = LTLTemplate('not_responded_existence')\n",
    "activities_a = [\"ER Triage\", \"CRP\", \"Leucocytes\"]\n",
    "activities_b = [\"Leucocytes\", \"Admission NC\", \"Release A\"]\n",
    "model = template.fill_template(activities_a, activities_b)\n",
    "print(f\"Formula: {model.formula}\")\n",
    "analyzer = LTLAnalyzer(event_log, model)\n",
    "conf_check_res_df = analyzer.run()\n",
    "conf_check_res_df"
   ],
   "outputs": [
    {
     "name": "stdout",
     "output_type": "stream",
     "text": [
      "Formula: F(con_ertriage || con_crp || con_leucocytes) ->  !(F(con_leucocytes || con_admissionnc || con_releasea))\n"
     ]
    },
    {
     "data": {
      "text/plain": [
       "     case:concept:name  accepted\n",
       "0                    A     False\n",
       "1                    B     False\n",
       "2                    C     False\n",
       "3                    D     False\n",
       "4                    E     False\n",
       "...                ...       ...\n",
       "1045               HNA     False\n",
       "1046               INA      True\n",
       "1047               JNA      True\n",
       "1048               KNA     False\n",
       "1049               LNA      True\n",
       "\n",
       "[1050 rows x 2 columns]"
      ],
      "text/html": [
       "<div>\n",
       "<style scoped>\n",
       "    .dataframe tbody tr th:only-of-type {\n",
       "        vertical-align: middle;\n",
       "    }\n",
       "\n",
       "    .dataframe tbody tr th {\n",
       "        vertical-align: top;\n",
       "    }\n",
       "\n",
       "    .dataframe thead th {\n",
       "        text-align: right;\n",
       "    }\n",
       "</style>\n",
       "<table border=\"1\" class=\"dataframe\">\n",
       "  <thead>\n",
       "    <tr style=\"text-align: right;\">\n",
       "      <th></th>\n",
       "      <th>case:concept:name</th>\n",
       "      <th>accepted</th>\n",
       "    </tr>\n",
       "  </thead>\n",
       "  <tbody>\n",
       "    <tr>\n",
       "      <th>0</th>\n",
       "      <td>A</td>\n",
       "      <td>False</td>\n",
       "    </tr>\n",
       "    <tr>\n",
       "      <th>1</th>\n",
       "      <td>B</td>\n",
       "      <td>False</td>\n",
       "    </tr>\n",
       "    <tr>\n",
       "      <th>2</th>\n",
       "      <td>C</td>\n",
       "      <td>False</td>\n",
       "    </tr>\n",
       "    <tr>\n",
       "      <th>3</th>\n",
       "      <td>D</td>\n",
       "      <td>False</td>\n",
       "    </tr>\n",
       "    <tr>\n",
       "      <th>4</th>\n",
       "      <td>E</td>\n",
       "      <td>False</td>\n",
       "    </tr>\n",
       "    <tr>\n",
       "      <th>...</th>\n",
       "      <td>...</td>\n",
       "      <td>...</td>\n",
       "    </tr>\n",
       "    <tr>\n",
       "      <th>1045</th>\n",
       "      <td>HNA</td>\n",
       "      <td>False</td>\n",
       "    </tr>\n",
       "    <tr>\n",
       "      <th>1046</th>\n",
       "      <td>INA</td>\n",
       "      <td>True</td>\n",
       "    </tr>\n",
       "    <tr>\n",
       "      <th>1047</th>\n",
       "      <td>JNA</td>\n",
       "      <td>True</td>\n",
       "    </tr>\n",
       "    <tr>\n",
       "      <th>1048</th>\n",
       "      <td>KNA</td>\n",
       "      <td>False</td>\n",
       "    </tr>\n",
       "    <tr>\n",
       "      <th>1049</th>\n",
       "      <td>LNA</td>\n",
       "      <td>True</td>\n",
       "    </tr>\n",
       "  </tbody>\n",
       "</table>\n",
       "<p>1050 rows × 2 columns</p>\n",
       "</div>"
      ]
     },
     "execution_count": 37,
     "metadata": {},
     "output_type": "execute_result"
    }
   ],
   "execution_count": 37
  },
  {
   "cell_type": "markdown",
   "metadata": {},
   "source": [
    "### `alternate_response`"
   ]
  },
  {
   "cell_type": "code",
   "metadata": {
    "ExecuteTime": {
     "end_time": "2026-05-29T14:01:02.196829300Z",
     "start_time": "2026-05-29T14:01:00.395530700Z"
    }
   },
   "source": [
    "template = LTLTemplate('alternate_response')\n",
    "activities_a = [\"ER Triage\", \"CRP\", \"Leucocytes\"]\n",
    "activities_b = [\"Leucocytes\", \"Admission NC\", \"Release A\"]\n",
    "model = template.fill_template(activities_a, activities_b)\n",
    "print(f\"Formula: {model.formula}\")\n",
    "analyzer = LTLAnalyzer(event_log, model)\n",
    "conf_check_res_df = analyzer.run()\n",
    "conf_check_res_df"
   ],
   "outputs": [
    {
     "name": "stdout",
     "output_type": "stream",
     "text": [
      "Formula: G((con_ertriage || con_crp || con_leucocytes) -> X[!]((!(con_ertriage || con_crp || con_leucocytes)U(con_leucocytes || con_admissionnc || con_releasea))))\n"
     ]
    },
    {
     "data": {
      "text/plain": [
       "     case:concept:name  accepted\n",
       "0                    A     False\n",
       "1                    B     False\n",
       "2                    C     False\n",
       "3                    D     False\n",
       "4                    E     False\n",
       "...                ...       ...\n",
       "1045               HNA     False\n",
       "1046               INA     False\n",
       "1047               JNA     False\n",
       "1048               KNA     False\n",
       "1049               LNA     False\n",
       "\n",
       "[1050 rows x 2 columns]"
      ],
      "text/html": [
       "<div>\n",
       "<style scoped>\n",
       "    .dataframe tbody tr th:only-of-type {\n",
       "        vertical-align: middle;\n",
       "    }\n",
       "\n",
       "    .dataframe tbody tr th {\n",
       "        vertical-align: top;\n",
       "    }\n",
       "\n",
       "    .dataframe thead th {\n",
       "        text-align: right;\n",
       "    }\n",
       "</style>\n",
       "<table border=\"1\" class=\"dataframe\">\n",
       "  <thead>\n",
       "    <tr style=\"text-align: right;\">\n",
       "      <th></th>\n",
       "      <th>case:concept:name</th>\n",
       "      <th>accepted</th>\n",
       "    </tr>\n",
       "  </thead>\n",
       "  <tbody>\n",
       "    <tr>\n",
       "      <th>0</th>\n",
       "      <td>A</td>\n",
       "      <td>False</td>\n",
       "    </tr>\n",
       "    <tr>\n",
       "      <th>1</th>\n",
       "      <td>B</td>\n",
       "      <td>False</td>\n",
       "    </tr>\n",
       "    <tr>\n",
       "      <th>2</th>\n",
       "      <td>C</td>\n",
       "      <td>False</td>\n",
       "    </tr>\n",
       "    <tr>\n",
       "      <th>3</th>\n",
       "      <td>D</td>\n",
       "      <td>False</td>\n",
       "    </tr>\n",
       "    <tr>\n",
       "      <th>4</th>\n",
       "      <td>E</td>\n",
       "      <td>False</td>\n",
       "    </tr>\n",
       "    <tr>\n",
       "      <th>...</th>\n",
       "      <td>...</td>\n",
       "      <td>...</td>\n",
       "    </tr>\n",
       "    <tr>\n",
       "      <th>1045</th>\n",
       "      <td>HNA</td>\n",
       "      <td>False</td>\n",
       "    </tr>\n",
       "    <tr>\n",
       "      <th>1046</th>\n",
       "      <td>INA</td>\n",
       "      <td>False</td>\n",
       "    </tr>\n",
       "    <tr>\n",
       "      <th>1047</th>\n",
       "      <td>JNA</td>\n",
       "      <td>False</td>\n",
       "    </tr>\n",
       "    <tr>\n",
       "      <th>1048</th>\n",
       "      <td>KNA</td>\n",
       "      <td>False</td>\n",
       "    </tr>\n",
       "    <tr>\n",
       "      <th>1049</th>\n",
       "      <td>LNA</td>\n",
       "      <td>False</td>\n",
       "    </tr>\n",
       "  </tbody>\n",
       "</table>\n",
       "<p>1050 rows × 2 columns</p>\n",
       "</div>"
      ]
     },
     "execution_count": 38,
     "metadata": {},
     "output_type": "execute_result"
    }
   ],
   "execution_count": 38
  },
  {
   "cell_type": "markdown",
   "metadata": {},
   "source": [
    "### `alternate_precedence`"
   ]
  },
  {
   "cell_type": "code",
   "metadata": {
    "ExecuteTime": {
     "end_time": "2026-05-29T14:01:06.180209800Z",
     "start_time": "2026-05-29T14:01:03.261571600Z"
    }
   },
   "source": [
    "template = LTLTemplate('alternate_precedence')\n",
    "activities_a = [\"ER Triage\", \"CRP\", \"Leucocytes\"]\n",
    "activities_b = [\"Leucocytes\", \"Admission NC\", \"Release A\"]\n",
    "model = template.fill_template(activities_a, activities_b)\n",
    "print(f\"Formula: {model.formula}\")\n",
    "analyzer = LTLAnalyzer(event_log, model)\n",
    "conf_check_res_df = analyzer.run()\n",
    "conf_check_res_df"
   ],
   "outputs": [
    {
     "name": "stdout",
     "output_type": "stream",
     "text": [
      "Formula: ((!(con_leucocytes || con_admissionnc || con_releasea))U(con_ertriage || con_crp || con_leucocytes))  && G((con_leucocytes || con_admissionnc || con_releasea) -> X[!]((!(con_leucocytes || con_admissionnc || con_releasea))U(con_ertriage || con_crp || con_leucocytes)) || G(!(con_leucocytes || con_admissionnc || con_releasea)))\n"
     ]
    },
    {
     "data": {
      "text/plain": [
       "     case:concept:name  accepted\n",
       "0                    A     False\n",
       "1                    B     False\n",
       "2                    C     False\n",
       "3                    D     False\n",
       "4                    E     False\n",
       "...                ...       ...\n",
       "1045               HNA     False\n",
       "1046               INA      True\n",
       "1047               JNA      True\n",
       "1048               KNA     False\n",
       "1049               LNA      True\n",
       "\n",
       "[1050 rows x 2 columns]"
      ],
      "text/html": [
       "<div>\n",
       "<style scoped>\n",
       "    .dataframe tbody tr th:only-of-type {\n",
       "        vertical-align: middle;\n",
       "    }\n",
       "\n",
       "    .dataframe tbody tr th {\n",
       "        vertical-align: top;\n",
       "    }\n",
       "\n",
       "    .dataframe thead th {\n",
       "        text-align: right;\n",
       "    }\n",
       "</style>\n",
       "<table border=\"1\" class=\"dataframe\">\n",
       "  <thead>\n",
       "    <tr style=\"text-align: right;\">\n",
       "      <th></th>\n",
       "      <th>case:concept:name</th>\n",
       "      <th>accepted</th>\n",
       "    </tr>\n",
       "  </thead>\n",
       "  <tbody>\n",
       "    <tr>\n",
       "      <th>0</th>\n",
       "      <td>A</td>\n",
       "      <td>False</td>\n",
       "    </tr>\n",
       "    <tr>\n",
       "      <th>1</th>\n",
       "      <td>B</td>\n",
       "      <td>False</td>\n",
       "    </tr>\n",
       "    <tr>\n",
       "      <th>2</th>\n",
       "      <td>C</td>\n",
       "      <td>False</td>\n",
       "    </tr>\n",
       "    <tr>\n",
       "      <th>3</th>\n",
       "      <td>D</td>\n",
       "      <td>False</td>\n",
       "    </tr>\n",
       "    <tr>\n",
       "      <th>4</th>\n",
       "      <td>E</td>\n",
       "      <td>False</td>\n",
       "    </tr>\n",
       "    <tr>\n",
       "      <th>...</th>\n",
       "      <td>...</td>\n",
       "      <td>...</td>\n",
       "    </tr>\n",
       "    <tr>\n",
       "      <th>1045</th>\n",
       "      <td>HNA</td>\n",
       "      <td>False</td>\n",
       "    </tr>\n",
       "    <tr>\n",
       "      <th>1046</th>\n",
       "      <td>INA</td>\n",
       "      <td>True</td>\n",
       "    </tr>\n",
       "    <tr>\n",
       "      <th>1047</th>\n",
       "      <td>JNA</td>\n",
       "      <td>True</td>\n",
       "    </tr>\n",
       "    <tr>\n",
       "      <th>1048</th>\n",
       "      <td>KNA</td>\n",
       "      <td>False</td>\n",
       "    </tr>\n",
       "    <tr>\n",
       "      <th>1049</th>\n",
       "      <td>LNA</td>\n",
       "      <td>True</td>\n",
       "    </tr>\n",
       "  </tbody>\n",
       "</table>\n",
       "<p>1050 rows × 2 columns</p>\n",
       "</div>"
      ]
     },
     "execution_count": 39,
     "metadata": {},
     "output_type": "execute_result"
    }
   ],
   "execution_count": 39
  }
 ],
 "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"
  }
 },
 "nbformat": 4,
 "nbformat_minor": 2
}