main_base.ipynb

{
  "nbformat": 4,
  "nbformat_minor": 2,
  "metadata": {
    "colab": {
      "name": "RA_project.ipynb",
      "provenance": [],
      "collapsed_sections": [],
      "toc_visible": true
    },
    "kernelspec": {
      "name": "python3",
      "display_name": "Python 3.7.7 64-bit ('base': conda)"
    },
    "language_info": {
      "name": "python",
      "version": "3.7.7",
      "mimetype": "text/x-python",
      "codemirror_mode": {
        "name": "ipython",
        "version": 3
      },
      "pygments_lexer": "ipython3",
      "nbconvert_exporter": "python",
      "file_extension": ".py"
    },
    "interpreter": {
      "hash": "fdcf986a19d66663db1a6faed0f4565f39e19bacafb44a8df11b713329195ec3"
    }
  },
  "cells": [
    {
      "cell_type": "markdown",
      "source": [
        "# LTL-f BASED-TRACE ALIGNMENT"
      ],
      "metadata": {
        "id": "N3zltNFvjHqi"
      }
    },
    {
      "cell_type": "code",
      "execution_count": 1,
      "source": [
        "import re\n",
        "from typing import Match, cast\n",
        "import copy\n",
        "import ast\n",
        "\n",
        "from ltlf2dfa.parser.ltlf import LTLfParser\n",
        "from dataclasses import dataclass\n",
        "from typing import Dict, Match, Set, Tuple, cast"
      ],
      "outputs": [],
      "metadata": {}
    },
    {
      "cell_type": "markdown",
      "source": [
        "## Constraint automata"
      ],
      "metadata": {
        "id": "UAFM4Xbhje6l"
      }
    },
    {
      "cell_type": "code",
      "execution_count": 2,
      "source": [
        "parser = LTLfParser()"
      ],
      "outputs": [],
      "metadata": {}
    },
    {
      "cell_type": "code",
      "execution_count": 3,
      "source": [
        "constraints =  [\"(!(q) & G((X(q) -> p)))\", \n",
        "                \"F(a)\",\n",
        "                \"((!(j) U i) | G(!(j)))\",\n",
        "                \"(F(e) -> F(f))\", \n",
        "                \"G((n -> X(o)))\"]\n",
        "\n",
        "constraints_10 = [\"(!(q) & G((X(q) -> p)))\", \n",
        "                    \"F(a)\", \n",
        "                    \"((!(j) U i) | G(!(j)))\", \n",
        "                    \"(F(e) -> F(f))\", \n",
        "                    \"G((n -> X(o)))\",\n",
        "                    \"!((F(s) & F(t)))\",\n",
        "                    \"G((t -> !(F(u))))\",\n",
        "                    \"G((v <-> !(X(w))))\",\n",
        "                    \"G(k -> F(l))\",\n",
        "                    \"!(F((b & X(F(b)))))\"]\n",
        "\n",
        "constraints_15 = [\"(!(q) & G((X(q) -> p)))\", \n",
        "                    \"F(a)\", \n",
        "                    \"((!(j) U i) | G(!(j)))\", \n",
        "                    \"(F(e) -> F(f))\", \n",
        "                    \"G((n -> X(o)))\",\n",
        "                    \"!((F(s) & F(t)))\",\n",
        "                    \"G((t -> !(F(u))))\",\n",
        "                    \"G((v <-> !(X(w))))\",\n",
        "                    \"G(k -> F(l))\",\n",
        "                    \"!(F((b & X(F(b)))))\",\n",
        "                    \"(!(r) & G((X(r) -> q)))\",\n",
        "                    \"G(h -> F(i))\",\n",
        "                    \"F(j)\",\n",
        "                    \"F(c)\",\n",
        "                    \"G((o -> X(p)))\"\n",
        "                    ]  \n",
        "constraints_20 = [\"(!(q) & G((X(q) -> p)))\", \n",
        "                    \"F(a)\", \n",
        "                    \"((!(j) U i) | G(!(j)))\", \n",
        "                    \"(F(e) -> F(f))\", \n",
        "                    \"G((n -> X(o)))\",\n",
        "                    \"!((F(s) & F(t)))\",\n",
        "                    \"G((t -> !(F(u))))\",\n",
        "                    \"G((v <-> !(X(w))))\",\n",
        "                    \"G(k -> F(l))\",\n",
        "                    \"!(F((b & X(F(b)))))\",\n",
        "                    \"(!(r) & G((X(r) -> q)))\",\n",
        "                    \"G(h -> F(i))\",\n",
        "                    \"F(j)\",\n",
        "                    \"F(c)\",\n",
        "                    \"G((o -> X(p)))\",\n",
        "                    \"((!(y) U x) | G(!(y)))\",\n",
        "                    \"F(x)\",\n",
        "                    \"G(c -> F(d))\",\n",
        "                    \"!(F((g & X(F(g)))))\",\n",
        "                    \"((!(m) U l) | G(!(m)))\"]    \n",
        "\n",
        "constraint_formulas = constraints"
      ],
      "outputs": [],
      "metadata": {}
    },
    {
      "cell_type": "markdown",
      "source": [
        "### Parse DFA with regular expressions"
      ],
      "metadata": {}
    },
    {
      "cell_type": "code",
      "execution_count": 4,
      "source": [
        "class StructureOutput():\n",
        "    def __init__(self, nb_states, variable_names, initial_state, accepting_states, rejecting_states, transitions): \n",
        "        self.nb_states = nb_states\n",
        "        self.variable_names = variable_names\n",
        "        self.initial_state = initial_state\n",
        "        self.accepting_states = accepting_states\n",
        "        self.rejecting_states = rejecting_states\n",
        "        self.transitions = transitions\n",
        "\n",
        "\n",
        "class StructureOutputRegex():\n",
        "\n",
        "    def __init__(self, output):\n",
        "        self.output = output\n",
        "\n",
        "    def total_function (self):\n",
        "        def create_transitions(self) -> Dict[int, Dict[int, Set[str]]]:\n",
        "            raw_transitions: Dict[int, Dict[int, Set[str]]] = {}\n",
        "            lines = self.output.splitlines()\n",
        "            # from the 8th line, the output specifies the transitions.\n",
        "            transition_strings = lines[7:]\n",
        "            for t in transition_strings:\n",
        "                match = cast(\n",
        "                    Match, re.search(\"State ([0-9]+): ([01X]+|) -> state ([0-9]+)\", t)\n",
        "                )\n",
        "                if match is None:\n",
        "                    continue\n",
        "                start_state = int(match.group(1))\n",
        "                guard = match.group(2)\n",
        "                end_state = int(match.group(3))\n",
        "                raw_transitions.setdefault(start_state, {}).setdefault(\n",
        "                    end_state, set()\n",
        "                ).add(guard)\n",
        "            return raw_transitions\n",
        "\n",
        "        variable_names : Tuple[str, ...] = tuple(cast(Match, re.search(\"DFA for formula with free variables: (.*)\", self.output),).group(1).split())\n",
        "        initial_state : int = int(cast(Match, re.search(\"Initial state: (.*)\\n\", self.output)).group(1))\n",
        "        accepting_states : Set[int] = set(map(int,cast(Match, re.search(\"Accepting states: (.*)\\n\", self.output)).group(1).split(),))\n",
        "        rejecting_states : Set[int] = set(map(int,cast(Match, re.search(\"Rejecting states: (.*)\\n\", self.output)).group(1).split(),))\n",
        "        nb_states : int = int(cast(Match,re.search(r\"Automaton has ([0-9]+) state(\\(?s\\)?)? and .* BDD-node(\\(?s\\)?)?\",self.output,),).group(1))\n",
        "        raw_transitions : Dict[int, Dict[int, Set[str]]] = create_transitions(self)\n",
        "        \n",
        "\n",
        "        return StructureOutput(nb_states, variable_names, initial_state, accepting_states, rejecting_states, raw_transitions)"
      ],
      "outputs": [],
      "metadata": {}
    },
    {
      "cell_type": "markdown",
      "source": [
        "### Build vocabulary of constraint automata"
      ],
      "metadata": {}
    },
    {
      "cell_type": "code",
      "execution_count": 5,
      "source": [
        "index = 1\n",
        "index_states = 0\n",
        "\n",
        "all_automata = {}\n",
        "\n",
        "for f in constraint_formulas:\n",
        "    build_automaton = {}\n",
        "    build_automaton[\"formula\"] = f\n",
        "\n",
        "    all_states_constr = []\n",
        "    final_states_constr = []\n",
        "    init_states_constr = []\n",
        "    rejecting_states_constr = []\n",
        "    rho_constr_basic = []\n",
        "    rho_tobe_negated = []\n",
        "    rho_tobe_positive = []\n",
        "\n",
        "    ## Parser + dfa #####################################################\n",
        "    formula = parser(f)       # returns an LTLfFormula\n",
        "    dfa = formula.to_dfa(mona_dfa_out=True)\n",
        "    mona_output = StructureOutputRegex(output=dfa).total_function() \n",
        "   \n",
        "    ## save all what is needed ##########################################\n",
        "    init_states_constr = 's'+str(index_states)\n",
        "    \n",
        "    states = set.union(mona_output.rejecting_states, mona_output.accepting_states)\n",
        "    states = list(states)\n",
        "    for elem in states:\n",
        "        all_states_constr.append('s'+str(elem+index_states))\n",
        "\n",
        "    for elem in list(mona_output.accepting_states):\n",
        "        final_states_constr.append('s'+str(elem+index_states))\n",
        "\n",
        "    alphabet = mona_output.variable_names\n",
        "\n",
        "    for key,elem in mona_output.transitions.items():\n",
        "        s_start = key + index_states\n",
        "        for k,e in elem.items():\n",
        "            s_end = k + index_states\n",
        "            sum = 0\n",
        "            comb = list(e)[0]\n",
        "            for char in comb:\n",
        "                if(char!='X'):\n",
        "                    sum += int(char)\n",
        "            if(sum > 1):\n",
        "                continue\n",
        "            elif(sum == 1):\n",
        "                index1 = comb.find('1')\n",
        "                rho_constr_basic.append(\"s\"+str(s_start)+\" \"+alphabet[index1]+\" s\"+str(s_end))\n",
        "            elif(sum == 0):\n",
        "                indeces0 = [i for i in range(len(comb)) if comb[i] in '0']\n",
        "                if (len(indeces0) == 0):\n",
        "                    indeces0 = [i for i in range(len(comb)) if comb[i] in 'X']\n",
        "                    res_list = [alphabet[i] for i in indeces0]\n",
        "                    rho_tobe_positive.append([s_start,s_end,res_list])\n",
        "                else:\n",
        "                    res_list = [alphabet[i] for i in indeces0]\n",
        "                    rho_tobe_negated.append([s_start,s_end,res_list])                 \n",
        "\n",
        "\n",
        "    build_automaton[\"all_states\"] = all_states_constr\n",
        "    build_automaton[\"final_states\"] = final_states_constr\n",
        "    build_automaton[\"init_state\"] = init_states_constr\n",
        "    build_automaton[\"transitions\"] = rho_constr_basic\n",
        "    build_automaton[\"symbols_constr\"] = alphabet\n",
        "    build_automaton[\"negated_transitions\"] = rho_tobe_negated\n",
        "    build_automaton[\"positive_transitions\"] = rho_tobe_positive\n",
        "\n",
        "    all_automata[\"a\"+str(index)] = build_automaton\n",
        "\n",
        "    index += 1\n",
        "    index_states += len(all_states_constr)"
      ],
      "outputs": [],
      "metadata": {}
    },
    {
      "cell_type": "markdown",
      "source": [
        "## Trace automata"
      ],
      "metadata": {}
    },
    {
      "cell_type": "markdown",
      "source": [
        "### Load xes file"
      ],
      "metadata": {
        "id": "I8Qh6gkJjR6R"
      }
    },
    {
      "cell_type": "code",
      "execution_count": 6,
      "source": [
        "log_paths = {}\n",
        "base_opt = \"base\"\n",
        "syn_real = \"created\" # or \"synthetic\"\n",
        "n_constr = [\"10\"]#, \"15\", \"20\"]\n",
        "choice = \"5\"\n",
        "constr_inverted = [\"3\", \"4\", \"6\"]\n",
        "len_traces = [\"1-50\", \"51-100\"]#, \"101-150\", \"151-200\"]\n",
        "\n",
        "for i in range(len(n_constr)):\n",
        "    for j in range(len(constr_inverted)):\n",
        "        for k in range(len(len_traces)):\n",
        "            key = choice+\"/\"+constr_inverted[j]+\"/\"+len_traces[k]\n",
        "            log_paths[key] = \"dataset/logs/\"+syn_real+\"-logs/\"+n_constr[i]+\"constraints/\"+constr_inverted[j]+\" constraints inverted/log-from-\"+n_constr[i]+\"constr-model-\"+constr_inverted[j]+\"constr_inverted-\"+len_traces[k]+\".xes\""
      ],
      "outputs": [],
      "metadata": {
        "id": "Otc3Rvi-2wXS"
      }
    },
    {
      "cell_type": "markdown",
      "source": [
        "### From xes files to traces as strings"
      ],
      "metadata": {}
    },
    {
      "cell_type": "code",
      "execution_count": 7,
      "source": [
        "alphabet = \"ABCDEFGHIJKLMNOPQRSTUVWXYZ\"\n",
        "voc = {}\n",
        "for i in range(len(alphabet)):\n",
        "    voc[i+1] = alphabet[i]\n",
        "\n",
        "def convertNumberToChar (val):\n",
        "    return voc[val]"
      ],
      "outputs": [],
      "metadata": {}
    },
    {
      "cell_type": "code",
      "execution_count": 8,
      "source": [
        "def readLog (log_path):\n",
        "    '''\n",
        "        flag:           True when we have to read an event from the file\n",
        "        trace:          List of events as integers\n",
        "        traceChar:      List of events as strings\n",
        "        traceString:    String of events\n",
        "        log:            List of all traces (as strings)\n",
        "    '''\n",
        "\n",
        "    flag = False\n",
        "    trace = []\n",
        "    traceChar = []\n",
        "    traceString = \"\"\n",
        "    log = []\n",
        "\n",
        "    f = open  (log_path)\n",
        "    f1 = f.readlines()\n",
        "    \n",
        "    for x in f1:\n",
        "        # if there is an event, we activate the flag\n",
        "        if (x.__contains__(\"<event>\")):\n",
        "            flag = True\n",
        "\n",
        "        # If flag is True and the name of the event is present,\n",
        "        # we extract the event name and append it to \"trace\"\n",
        "        if (flag and x.__contains__('<string key=\"concept:name\"')):\n",
        "            val = x.split('value=\"activity ',1)[1]\n",
        "            val = val.split('\"')[0]                \n",
        "            trace.append(val)\n",
        "            flag = False\n",
        "\n",
        "        # When the trace is terminated, we can convert the numbers in strings\n",
        "        if (x.__contains__(\"</trace>\")):\n",
        "            for event in trace:\n",
        "                traceChar.append(convertNumberToChar(int(event)))\n",
        "            traceString = \"\".join(traceChar)\n",
        "            log.append(traceString)\n",
        "\n",
        "            # Reset variables\n",
        "            trace = []\n",
        "            traceChar = []\n",
        "            traceString = \"\"\n",
        "    \n",
        "    return log"
      ],
      "outputs": [],
      "metadata": {
        "id": "944iEX333Q2E"
      }
    },
    {
      "cell_type": "markdown",
      "source": [
        "### Build vocabulary of trace automata"
      ],
      "metadata": {}
    },
    {
      "cell_type": "code",
      "execution_count": 9,
      "source": [
        "if (syn_real == \"synthetic\"):\n",
        "    all_traces_log = copy.deepcopy(log_paths)\n",
        "    all_automata_log = {}\n",
        "\n",
        "    for k, log_path in log_paths.items():\n",
        "        traces_log = readLog(log_path) # list of traces\n",
        "\n",
        "        all_traces = {}\n",
        "        variabili = {}\n",
        "\n",
        "        idx_trace = 1\n",
        "\n",
        "        for t in traces_log:\n",
        "            trace = {}\n",
        "            variabile = copy.deepcopy(all_automata)\n",
        "            \n",
        "            symbols_trace = list(set(t))\n",
        "            \n",
        "            ## Build trace automaton ###################################\n",
        "            rho_trace_basic = []\n",
        "            Q_trace = []\n",
        "            for i in range(len(t)):\n",
        "                Q_trace.append('t'+str(i))\n",
        "                rho_trace_basic.append('t'+str(i)+\" \"+t[i] +\" \"+ 't'+str(i+1))\n",
        "\n",
        "            Q_trace.append('t'+str(len(t)))\n",
        "            init_state_trace = Q_trace[0]\n",
        "            final_state_trace = Q_trace[-1]\n",
        "\n",
        "            trace[\"symbols_trace\"] = symbols_trace\n",
        "            trace[\"init_state_trace\"] = init_state_trace\n",
        "            trace[\"final_state_trace\"] = final_state_trace\n",
        "            trace[\"Q_trace\"] = Q_trace\n",
        "            trace[\"rho_trace_basic\"] = rho_trace_basic\n",
        "\n",
        "            all_traces[idx_trace] = trace\n",
        "\n",
        "            ## Now we add the transitions for the negated symbols ######\n",
        "\n",
        "            for ID,automaton in all_automata.items():\n",
        "                symb_constr = set(variabile[ID][\"symbols_constr\"])\n",
        "                symb_trace = set(symbols_trace)\n",
        "                all_symbs = list(set.union(symb_constr, symb_trace))\n",
        "\n",
        "                trans = copy.deepcopy(automaton[\"transitions\"])\n",
        "                for t_neg in variabile[ID][\"negated_transitions\"]:\n",
        "                    symbs = copy.deepcopy(all_symbs)\n",
        "                    for t in t_neg[2]:\n",
        "                        symbs.remove(t)\n",
        "                    for elem in symbs:\n",
        "                        if (\"s\"+str(t_neg[0])+\" \"+elem+\" s\"+str(t_neg[1]) not in trans):\n",
        "                            trans.append(\"s\"+str(t_neg[0])+\" \"+elem+\" s\"+str(t_neg[1]))\n",
        "\n",
        "                for t_pos in variabile[ID][\"positive_transitions\"]:\n",
        "                    symbs = copy.deepcopy(all_symbs)\n",
        "                    for elem in symbs:\n",
        "                        if (\"s\"+str(t_pos[0])+\" \"+elem+\" s\"+str(t_pos[1]) not in trans):\n",
        "                            trans.append(\"s\"+str(t_pos[0])+\" \"+elem+\" s\"+str(t_pos[1]))\n",
        "\n",
        "                variabile[ID][\"transitions\"] = trans\n",
        "            \n",
        "            variabili[idx_trace] = variabile\n",
        "\n",
        "            idx_trace += 1\n",
        "\n",
        "        all_automata_log[k] = variabili\n",
        "        \n",
        "        all_traces_log[k] = all_traces\n",
        "\n",
        "elif (syn_real == \"created\"):\n",
        "    all_traces_log = {}\n",
        "    all_automata_log = {}\n",
        "\n",
        "    for range_lenght in len_traces:\n",
        "        k = choice+\"/\"+\"0\"+\"/\"+range_lenght\n",
        "\n",
        "        f = open(\"dataset/logs/created-logs/\"+range_lenght+\".txt\", \"r\")\n",
        "\n",
        "        traces_log = ast.literal_eval(f.read()) # list of traces\n",
        "\n",
        "        all_traces = {}\n",
        "        variabili = {}\n",
        "\n",
        "        idx_trace = 1\n",
        "\n",
        "        for t in traces_log:\n",
        "            trace = {}\n",
        "            variabile = copy.deepcopy(all_automata)\n",
        "            \n",
        "            symbols_trace = list(set(t))\n",
        "            \n",
        "            ## Build trace automaton ###################################\n",
        "            rho_trace_basic = []\n",
        "            Q_trace = []\n",
        "            for i in range(len(t)):\n",
        "                Q_trace.append('t'+str(i))\n",
        "                rho_trace_basic.append('t'+str(i)+\" \"+t[i] +\" \"+ 't'+str(i+1))\n",
        "\n",
        "            Q_trace.append('t'+str(len(t)))\n",
        "            init_state_trace = Q_trace[0]\n",
        "            final_state_trace = Q_trace[-1]\n",
        "\n",
        "            trace[\"symbols_trace\"] = symbols_trace\n",
        "            trace[\"init_state_trace\"] = init_state_trace\n",
        "            trace[\"final_state_trace\"] = final_state_trace\n",
        "            trace[\"Q_trace\"] = Q_trace\n",
        "            trace[\"rho_trace_basic\"] = rho_trace_basic\n",
        "\n",
        "            all_traces[idx_trace] = trace\n",
        "\n",
        "            ## Now we add the transitions for the negated symbols ######\n",
        "\n",
        "            for ID,automaton in all_automata.items():\n",
        "                symb_constr = set(variabile[ID][\"symbols_constr\"])\n",
        "                symb_trace = set(symbols_trace)\n",
        "                all_symbs = list(set.union(symb_constr, symb_trace))\n",
        "\n",
        "                trans = copy.deepcopy(automaton[\"transitions\"])\n",
        "                for t_neg in variabile[ID][\"negated_transitions\"]:\n",
        "                    symbs = copy.deepcopy(all_symbs)\n",
        "                    for t in t_neg[2]:\n",
        "                        symbs.remove(t)\n",
        "                    for elem in symbs:\n",
        "                        if (\"s\"+str(t_neg[0])+\" \"+elem+\" s\"+str(t_neg[1]) not in trans):\n",
        "                            trans.append(\"s\"+str(t_neg[0])+\" \"+elem+\" s\"+str(t_neg[1]))\n",
        "\n",
        "                for t_pos in variabile[ID][\"positive_transitions\"]:\n",
        "                    symbs = copy.deepcopy(all_symbs)\n",
        "                    for elem in symbs:\n",
        "                        if (\"s\"+str(t_pos[0])+\" \"+elem+\" s\"+str(t_pos[1]) not in trans):\n",
        "                            trans.append(\"s\"+str(t_pos[0])+\" \"+elem+\" s\"+str(t_pos[1]))\n",
        "\n",
        "                variabile[ID][\"transitions\"] = trans\n",
        "            \n",
        "            variabili[idx_trace] = variabile\n",
        "\n",
        "            idx_trace += 1\n",
        "\n",
        "        all_automata_log[k] = variabili\n",
        "        \n",
        "        all_traces_log[k] = all_traces"
      ],
      "outputs": [],
      "metadata": {}
    },
    {
      "cell_type": "markdown",
      "source": [
        "## PDDL"
      ],
      "metadata": {}
    },
    {
      "cell_type": "code",
      "execution_count": 10,
      "source": [
        "for key,all_traces in all_traces_log.items():\n",
        "    n_cons, inv, lenght = key.split('/')\n",
        "    type_db = n_cons+\"_\"+inv+\"_\"+lenght\n",
        "    \n",
        "    for id_trace, trace in all_traces.items():\n",
        "        all_automata = copy.deepcopy(all_automata_log[key][id_trace])\n",
        "\n",
        "        all_states_constr = []\n",
        "        for ID,a in all_automata.items():\n",
        "            for elem in a['all_states']:\n",
        "                all_states_constr.append(elem)\n",
        "\n",
        "        symbols_tot = []\n",
        "        for ID,a in all_automata.items():\n",
        "            for s in a[\"symbols_constr\"]:\n",
        "                symbols_tot.append(s)\n",
        "        symbols_tot = list(set(symbols_tot).union(set(trace[\"symbols_trace\"])))\n",
        "        \n",
        "        # DOMAIN ###########################################################################\n",
        "        domain_name = \"domain_\"+base_opt+\"_\"+type_db+\"_trace\"+str(id_trace)\n",
        "\n",
        "        pddl_domain_initial = \"(define (domain \"+domain_name+\") \"\\\n",
        "                        \"(:requirements :strips :typing :action-costs) \"\\\n",
        "                        \"(:types trace_state automaton_state - state activity automaton_name) \"\n",
        "\n",
        "        pddl_domain_predicates = \"(:predicates (trace ?t1 - trace_state \"\\\n",
        "                                    \"?e - activity \"\\\n",
        "                                    \"?t2 - trace_state) \"\\\n",
        "                                    \"(automaton \"\\\n",
        "                                    \"?s1 - automaton_state \"\\\n",
        "                                    \"?e - activity \"\\\n",
        "                                    \"?s2 - automaton_state) \"\\\n",
        "                                    \"(cur_state ?s - state) \"\\\n",
        "                                    \"(final_state ?s - state)) \"\\\n",
        "                                    \"(:functions (total-cost)) \"\n",
        "\n",
        "\n",
        "        pddl_domain_actions =  \"(:action sync \"\\\n",
        "                                \":parameters (?t1 - trace_state ?e - activity ?t2 - trace_state) \"\\\n",
        "                                \":precondition (and (cur_state ?t1) (trace ?t1 ?e ?t2)) \"\\\n",
        "                                \":effect (and (not (cur_state ?t1)) (cur_state ?t2) \"\\\n",
        "                                \"(forall (?s1 ?s2 - automaton_state) \"\\\n",
        "                                \"(when (and (cur_state ?s1) \"\\\n",
        "                                \"(automaton ?s1 ?e ?s2)) \"\\\n",
        "                                \"(and (not (cur_state ?s1)) \"\\\n",
        "                                \"(cur_state ?s2)))))) \"\\\n",
        "                                \"(:action add \"\\\n",
        "                                \":parameters (?e - activity ?s1 ?s2 - state) \"\\\n",
        "                                \":effect (and (increase (total-cost) 1) \"\\\n",
        "                                \"(forall (?s1 ?s2 - automaton_state) \"\\\n",
        "                                \"(when (and (cur_state ?s1) \"\\\n",
        "                                \"(automaton ?s1 ?e ?s2)) \"\\\n",
        "                                \"(and (not (cur_state ?s1)) \"\\\n",
        "                                \"(cur_state ?s2)))))) \"\\\n",
        "                                \"(:action del \"\\\n",
        "                                \":parameters (?t1 - trace_state ?e - activity \"\\\n",
        "                                \"?t2 - trace_state) \"\\\n",
        "                                \":precondition (and (cur_state ?t1) (trace ?t1 ?e ?t2)) \"\\\n",
        "                                \":effect (and (increase (total-cost) 1) \"\\\n",
        "                                \"(not (cur_state ?t1)) (cur_state ?t2))))\"\n",
        "\n",
        "        pddl_domain = pddl_domain_initial + pddl_domain_predicates + pddl_domain_actions\n",
        "        \n",
        "        # PROBLEM ###########################################################################\n",
        "        problem_name = \"problem_\"+base_opt+\"_\"+type_db+\"_trace\"+str(id_trace)\n",
        "        pddl_problem_initial = \"(define (problem \"+problem_name+\") (:domain \"+domain_name+\") \"\n",
        "        pddl_problem_objects = \"(:objects \"\n",
        "\n",
        "        for q in trace[\"Q_trace\"]:\n",
        "            pddl_problem_objects += q+\" \"\n",
        "        pddl_problem_objects += \"- trace_state \"\n",
        "\n",
        "\n",
        "        for q in all_states_constr:\n",
        "            pddl_problem_objects += q+\" \"\n",
        "        pddl_problem_objects += \"- automaton_state \"\n",
        "\n",
        "\n",
        "        for s in symbols_tot:\n",
        "            pddl_problem_objects += s+\" \"\n",
        "        pddl_problem_objects += \"- activity\"\n",
        "\n",
        "        pddl_problem_objects += \") \"\n",
        "\n",
        "\n",
        "        pddl_problem_init = \"(:init (= (total-cost) 0) (cur_state \"+trace[\"init_state_trace\"]+\") \"\n",
        "        for t in trace[\"rho_trace_basic\"]:\n",
        "            pddl_problem_init += \"(trace \"+t+\") \"\n",
        "        pddl_problem_init += \"(final_state \"+trace[\"final_state_trace\"]+\") \"\n",
        "\n",
        "        for ID, a in all_automata.items():\n",
        "            pddl_problem_init += \"(cur_state \"+a[\"init_state\"]+\") \" \n",
        "            for t in a[\"transitions\"]:\n",
        "                pddl_problem_init += \"(automaton \"+t+\") \"\n",
        "\n",
        "            for i in range(len(a[\"final_states\"])):\n",
        "                pddl_problem_init += \"(final_state \"+a[\"final_states\"][i]+\") \"\n",
        "        pddl_problem_init += \") \"\n",
        "\n",
        "\n",
        "        pddl_problem_goal = \"(:goal (forall (?s - state) \"\\\n",
        "                            \"(imply (cur_state ?s) (final_state ?s)))) \"\n",
        "        pddl_problem_metric = \"(:metric minimize (total-cost)))\"\n",
        "        pddl_problem = pddl_problem_initial + pddl_problem_objects + pddl_problem_init + pddl_problem_goal + pddl_problem_metric\n",
        "\n",
        "        # SAVE ########################################################################\n",
        "        file1 = open(\"PDDL/\"+syn_real+\"/\"+base_opt+\"/\"+domain_name+\".pddl\", \"w\")\n",
        "        file1.write(pddl_domain)\n",
        "        file1.close()\n",
        "\n",
        "        file2 = open(\"PDDL/\"+syn_real+\"/\"+base_opt+\"/\"+problem_name+\".pddl\", \"w\")\n",
        "        file2.write(pddl_problem)\n",
        "        file2.close()\n",
        "\n",
        "        id_trace += 1"
      ],
      "outputs": [],
      "metadata": {
        "colab": {
          "base_uri": "https://localhost:8080/"
        },
        "id": "fq0E10UEQ2KN",
        "outputId": "625d168f-b794-402f-dfc3-6944fe96a730"
      }
    },
    {
      "cell_type": "markdown",
      "source": [
        "Fast-downward planner:\n",
        "`./fast-downward.py domain_multi.pddl problem_multi.pddl --search \"astar(blind())\"`"
      ],
      "metadata": {}
    }
  ]
}