Economics to TLA+ Business Patterns

Этот репозиторий представляет собой уникальный проект по переводу классического учебника по макро- и микроэкономике (26 глав) в строгие математические и логические модели на языке TLA+.

Главная цель проекта — дать предпринимателям, CEO и системным архитекторам набор готовых "лего-блоков" для моделирования, симуляции и стресс-тестирования бизнес-процессов, стратегий ценообразования и макроэкономических рисков.

📂 Структура проекта

├── Business_Patterns_TLA/      # Основная библиотека: 25 паттернов + TLA+ код
│   ├── 01_Basics_and_Markets/             # Микроэкономика, воронки, цены, ROI
│   ├── 02_Public_Sector_and_Externalities/# Налоги, экстерналии, общие ресурсы
│   ├── 03_Firms_and_Competition/          # Масштабирование, монополии, теория игр
│   ├── 04_Labor_and_Information/          # Найм, рынок "лимонов", асимметрия
│   ├── 05_Macroeconomics_and_Crises/      # Инфляция, ВВП, "Черные лебеди", пузыри
│   ├── principles/                        # Исполняемые файлы .tla и .cfg
│   └── README.md                          # Подробный каталог всех паттернов
│
├── source_chapters/            # Исходные текстовые конспекты 26 глав учебника
│
├── traces_bin/                 # Служебная папка: бинарные трейсы работы Model Checker
│
└── tla2tools.jar               # Исполняемый файл TLA+ Toolbox (Model Checker)

🧠 Что такое TLA+ Бизнес-Паттерны?

Вместо того чтобы изучать экономику в теории, мы формализовали каждый закон в алгоритм. Например:

• Закон спроса и предложения превратился в алгоритм динамического ценообразования (Dynamic Pricing).
• Сравнительное преимущество стало математическим доказательством того, почему CEO должен делегировать задачи аутсорсу.
• Закон убывающей отдачи стал моделью для расчета идеального размера IT-команды (обоснование Закона Брукса).
• Дилемма заключенного переложена на ценовые войны между корпорациями-олигополиями.

Подробное описание каждого из 25 паттернов вы найдете в каталоге библиотеки.

🚀 Как запускать модели (Model Checking)

Каждый паттерн сопровождается файлом конфигурации (.cfg) с математическим инвариантом (проверкой гипотезы). Чтобы запустить симуляцию и увидеть, как экономический закон работает на практике:

1. Убедитесь, что у вас установлена Java (JRE).
2. Выполните команду запуска TLC Model Checker из корня проекта:

# Пример: Запуск модели Воронки Продаж
java -cp tla2tools.jar tlc2.TLC Business_Patterns_TLA/principles/Pattern_04_Funnel.tla

# Пример: Проверка уязвимости к Финансовым Пузырям
java -cp tla2tools.jar tlc2.TLC Business_Patterns_TLA/principles/Pattern_23_FinancialBubbles.tla

Чекер переберет все возможные состояния (сотни тысяч вариантов развития бизнеса) и выдаст математически доказанный путь достижения цели (или причину неизбежного банкротства).