MFES_Ficha_1.ipynb

{
  "nbformat": 4,
  "nbformat_minor": 0,
  "metadata": {
    "colab": {
      "provenance": []
    },
    "kernelspec": {
      "name": "python3",
      "display_name": "Python 3"
    },
    "language_info": {
      "name": "python"
    }
  },
  "cells": [
    {
      "cell_type": "markdown",
      "source": [
        "**PG54469**, **Edgar Wchua Pires Guilherme**, Mestrado em Engenharia Informática\n",
        "\n",
        "**MFES** - Métodos Formais em Engenharia de Software"
      ],
      "metadata": {
        "id": "flHEpRZkgq1z"
      }
    },
    {
      "cell_type": "markdown",
      "source": [
        "\n",
        "\n",
        "---\n",
        "**Ficha 1**\n",
        "\n",
        "**Modelação em Lógica Proposicional**\n",
        "\n",
        "https://haslab.github.io/MFES/2324/ficha-1.pdf\n",
        "\n"
      ],
      "metadata": {
        "id": "Y9o1wDy7hdSr"
      }
    },
    {
      "cell_type": "markdown",
      "source": [
        "\n",
        "\n",
        "---\n",
        "\n",
        "**Instalação das bibliotecas**"
      ],
      "metadata": {
        "id": "i-69U0aYhSWK"
      }
    },
    {
      "cell_type": "code",
      "source": [
        "!pip install z3-solver"
      ],
      "metadata": {
        "colab": {
          "base_uri": "https://localhost:8080/"
        },
        "id": "tnC2TNJshEFV",
        "outputId": "83dd06ce-a933-4c39-c46d-8478eee14ad8"
      },
      "execution_count": 1,
      "outputs": [
        {
          "output_type": "stream",
          "name": "stdout",
          "text": [
            "Collecting z3-solver\n",
            "  Downloading z3_solver-4.12.2.0-py2.py3-none-manylinux2014_x86_64.whl (55.7 MB)\n",
            "\u001b[2K     \u001b[90m━━━━━━━━━━━━━━━━━━━━━━━━━━━━━━━━━━━━━━━━\u001b[0m \u001b[32m55.7/55.7 MB\u001b[0m \u001b[31m10.3 MB/s\u001b[0m eta \u001b[36m0:00:00\u001b[0m\n",
            "\u001b[?25hInstalling collected packages: z3-solver\n",
            "Successfully installed z3-solver-4.12.2.0\n"
          ]
        }
      ]
    },
    {
      "cell_type": "markdown",
      "source": [
        "---\n",
        "\n",
        "**Exercício 1 - Configuração de produtos**\n",
        "\n",
        "\n",
        "1. Codificar as dependências entre configurações como uma fórmula proposicional ψ.\n",
        "2. Codificar as opções selecionadas pelo cliente como uma fórmula proposicional φ.\n",
        "3. Usar o SAT solver para verificar se ψ ∧ φ não é contraditório.\n",
        "Considere agora a seguinte dependência entre as configuraçõoes disponíveis para a personalização de um automóvel:\n",
        "\n",
        "“O ar condicionado **Thermotronic comfort** *requer* uma **bateria de alta capacidade**,\n",
        "*exceto* quando *combinado* com **motores a gasolina de 3,2 litros**.”\n",
        "\n",
        "Será que um cliente pode *escolher* o ar condicionado **Thermotronic comfort**, uma **bateria de pequena capacidade**, mas *não escolher* o **motor de 3,2 litros**? Como poderia responder a esta pergunta com a ajuda de um SAT solver?"
      ],
      "metadata": {
        "id": "K8uIiUB-hp5V"
      }
    },
    {
      "cell_type": "code",
      "source": [
        "from z3 import *\n",
        "\n",
        "thermotronic_comfort = Bool('Thermotronic comfort')\n",
        "bateria_alta_capacidade = Bool(\"bateria de alta capacidade\")\n",
        "bateria_pequena_capacidade = Bool(\"bateria de pequena capacidade\")\n",
        "motor_gasolina_3_2 = Bool(\"motores a gasolina de 3,2 litros\")\n",
        "\n",
        "s = Solver()\n",
        "\n",
        "# O ar condicionado Thermotronic comfort requer uma bateria de alta capacidade\n",
        "# exceto quando combinado com motores a gasolina de 3,2 litros\n",
        "s.add(Implies(And(thermotronic_comfort, Not(motor_gasolina_3_2)), bateria_alta_capacidade))\n",
        "\n",
        "s.add(Implies(bateria_alta_capacidade, Not(bateria_pequena_capacidade)))\n",
        "\n",
        "print('Teste da escolha do cliente')\n",
        "s.push()\n",
        "\n",
        "s.add(thermotronic_comfort)\n",
        "s.add(bateria_pequena_capacidade)\n",
        "s.add(Not(motor_gasolina_3_2))\n",
        "\n",
        "r = s.check()\n",
        "\n",
        "if r == sat:\n",
        "    print(s.model())\n",
        "    print('O cliente pode escolher o ar condicionado Thermotronic comfort, uma bateria de pequena capacidade, mas não escolher o motor de 3,2 litros')\n",
        "else:\n",
        "    print('O cliente não pode escolher o ar condicionado Thermotronic comfort, uma bateria de pequena capacidade, mas não escolher o motor de 3,2 litros')\n",
        "\n",
        "s.pop()\n"
      ],
      "metadata": {
        "colab": {
          "base_uri": "https://localhost:8080/"
        },
        "id": "VOmapkKflGk_",
        "outputId": "b760f4a2-c6cb-44b9-927b-2d1996158bc7"
      },
      "execution_count": 10,
      "outputs": [
        {
          "output_type": "stream",
          "name": "stdout",
          "text": [
            "Teste da escolha do cliente\n",
            "O cliente não pode escolher o ar condicionado Thermotronic comfort, uma bateria de pequena capacidade, mas não escolher o motor de 3,2 litros\n"
          ]
        }
      ]
    },
    {
      "cell_type": "markdown",
      "source": [
        "---\n",
        "\n",
        "**Exercício 2 - Distribuição de gabinetes**\n",
        "\n",
        "Considere que temos 3 gabinetes e queremos\n",
        "distribuir 4 pessoas (Ana=1, Nuno=2, Pedro=3 e Maria=4) por esses gabinetes.\n",
        "\n",
        "Considere que foram estipuladas as seguintes regras de ocupação dos gabinetes:\n",
        "\n",
        "(a) Cada pessoa ocupa um único gabinete.\n",
        "\n",
        "(b) O Nuno e o Pedro não podem partilhar gabinete.\n",
        "\n",
        "(c) Se a Ana ficar sozinha num gabinete, então o Pedro também terá que ficar sozinho num gabinete.\n",
        "\n",
        "(d) Cada gabinete só pode acomodar, no máximo, 2 pessoas.\n"
      ],
      "metadata": {
        "id": "nzNB95oopNL2"
      }
    },
    {
      "cell_type": "code",
      "source": [
        "gabinetes = [1, 2, 3]\n",
        "pessoas = [\"Ana\", \"Nuno\", \"Pedro\", \"Maria\"]\n",
        "n_pessoas = len(pessoas)\n",
        "n_gabinetes = len(gabinetes)\n",
        "\n",
        "x = {}\n",
        "for p in pessoas:\n",
        "  x[p] = {}\n",
        "  for g in gabinetes:\n",
        "    x[p][g] = Bool(\"%s - %s\" % (p, g))\n",
        "\n",
        "s = Solver()\n",
        "\n",
        "# Cada pessoa ocupa pelo menos um gabinete.\n",
        "for p in pessoas:\n",
        "  s.add(Or([x[p][g] for g in gabinetes]))\n",
        "\n",
        "\n",
        "# Cada pessoa ocupa um único gabinete\n",
        "# for p in pessoas:\n",
        "#   for i in range(n_gabinetes - 1):\n",
        "#     for j in range(i + 1, n_gabinetes):\n",
        "#       s.add(Implies(x[p][i], Not(x[p][j])))\n",
        "for p in pessoas:\n",
        "  for g in gabinetes:\n",
        "    s.add([Implies(x[p][g], Not(x[p][j])) for j in gabinetes if j > g])\n",
        "\n",
        "\n",
        "# O Nuno e o Pedro não podem partilhar gabinete\n",
        "def nao_pode_partilhar_gabinete(p1, p2):\n",
        "    return And([Implies(x[p1][g], Not(x[p2][g])) for g in gabinetes])\n",
        "\n",
        "s.add(nao_pode_partilhar_gabinete(\"Nuno\", \"Pedro\"))\n",
        "\n",
        "# Se a Ana ficar sozinha num gabinete, então o Pedro também terá que ficar sozinho num gabinete\n",
        "def fica_sozinho_no_gabinete(p):\n",
        "    return And([Implies(x[p][g], And([Not(x[i][g]) for i in pessoas if i != p])) for g in gabinetes])\n",
        "\n",
        "s.add(Implies(fica_sozinho_no_gabinete(\"Ana\"), fica_sozinho_no_gabinete(\"Pedro\")))\n",
        "\n",
        "# Cada gabinete só pode acomodar, no máximo, 2 pessoas.\n",
        "def maximo_2_pessoas_por_gabinete(g):\n",
        "  for a in pessoas:\n",
        "    for b in [i for i in pessoas if i != a]:\n",
        "        s.add(Implies(And(x[a][g], x[b][g]), And([Not(x[c][g]) for c in pessoas if c not in [a, b]])))\n",
        "\n",
        "for g in gabinetes:\n",
        "  maximo_2_pessoas_por_gabinete(g)\n",
        "\n",
        "# Solve\n",
        "if s.check() == sat:\n",
        "    m = s.model()\n",
        "    for p in pessoas:\n",
        "        for g in gabinetes:\n",
        "            if is_true(m[x[p][g]]):\n",
        "                print(\"%s fica no gabinete %s\" % (p,g))\n",
        "else:\n",
        "  print(\"Não tem solução.\")"
      ],
      "metadata": {
        "colab": {
          "base_uri": "https://localhost:8080/"
        },
        "id": "N4_VvgjJrXbc",
        "outputId": "6ac114f7-ecdc-4340-c7c3-d2a64964494e"
      },
      "execution_count": 23,
      "outputs": [
        {
          "output_type": "stream",
          "name": "stdout",
          "text": [
            "Ana fica no gabinete 2\n",
            "Nuno fica no gabinete 2\n",
            "Pedro fica no gabinete 1\n",
            "Maria fica no gabinete 3\n"
          ]
        }
      ]
    }
  ]
}