Add examples, documentation, and build scripts

Co-authored-by: johndoe6345789 <224850594+johndoe6345789@users.noreply.github.com>
2026-04-24 13:45:03 +00:00 · 2025-12-27 02:59:38 +00:00
parent 39e52e0363
commit ed016de7f8
8 changed files with 828 additions and 0 deletions
--- a/CONTRIBUTING.md
+++ b/CONTRIBUTING.md
@@ -0,0 +1,294 @@
+# Contributing to TLA+ Visualiser
+
+Thank you for your interest in contributing! This document provides guidelines and instructions for contributing to the project.
+
+## Code of Conduct
+
+- Be respectful and inclusive
+- Welcome newcomers and help them learn
+- Focus on constructive feedback
+- Respect different viewpoints and experiences
+
+## Getting Started
+
+1. **Fork the repository** on GitHub
+2. **Clone your fork** locally:
+   ```bash
+   git clone https://github.com/YOUR_USERNAME/tla_visualiser.git
+   cd tla_visualiser
+   ```
+3. **Set up development environment** (see [BUILDING.md](docs/BUILDING.md))
+4. **Create a branch** for your work:
+   ```bash
+   git checkout -b feature/my-new-feature
+   ```
+
+## Development Workflow
+
+### 1. Making Changes
+
+- Keep changes focused and atomic
+- Follow existing code style
+- Add tests for new functionality
+- Update documentation as needed
+
+### 2. Code Style
+
+#### C++
+- Follow C++20 best practices
+- Use meaningful variable names
+- Prefer `const` where applicable
+- Use smart pointers over raw pointers
+- RAII for resource management
+
+**Example:**
+```cpp
+// Good
+auto importer = std::make_unique<GitHubImporter>();
+const auto url_info = importer->parseUrl(url);
+
+// Avoid
+GitHubImporter* importer = new GitHubImporter();
+auto url_info = importer->parseUrl(url);
+delete importer;
+```
+
+#### QML
+- Use consistent indentation (4 spaces)
+- Group properties logically
+- Use property bindings where appropriate
+- Add comments for complex logic
+
+**Example:**
+```qml
+Rectangle {
+    id: root
+    
+    // Size properties
+    width: 200
+    height: 100
+    
+    // Visual properties
+    color: "#f0f0f0"
+    border.color: "#cccccc"
+    border.width: 1
+    
+    // Content
+    Text {
+        anchors.centerIn: parent
+        text: "Hello"
+    }
+}
+```
+
+### 3. Commits
+
+Write clear, descriptive commit messages:
+
+```
+Short summary (50 chars or less)
+
+More detailed explanation if needed. Wrap at 72 characters.
+Explain what changes were made and why.
+
+- Bullet points are okay
+- Use imperative mood: "Add feature" not "Added feature"
+```
+
+### 4. Testing
+
+Always test your changes:
+
+```bash
+# Build
+cmake --build build --config Release
+
+# Run tests
+cd build
+ctest --output-on-failure
+
+# Run specific test
+./tests/test_github_importer
+```
+
+#### Writing Tests
+
+Add tests for new functionality:
+
+```cpp
+#include <QtTest/QtTest>
+#include "my_class.h"
+
+class TestMyClass : public QObject
+{
+    Q_OBJECT
+
+private slots:
+    void testFeature();
+};
+
+void TestMyClass::testFeature()
+{
+    MyClass obj;
+    QCOMPARE(obj.getValue(), 42);
+}
+
+QTEST_MAIN(TestMyClass)
+#include "test_my_class.moc"
+```
+
+### 5. Documentation
+
+Update documentation for:
+- New features
+- API changes
+- Build requirements
+- Usage instructions
+
+Documentation locations:
+- `README.md`: Overview and quick start
+- `docs/BUILDING.md`: Build instructions
+- `docs/ARCHITECTURE.md`: Architecture details
+- Code comments: Public API and complex logic
+
+## Pull Request Process
+
+### 1. Before Submitting
+
+- [ ] Code builds successfully
+- [ ] All tests pass
+- [ ] New tests added for new features
+- [ ] Documentation updated
+- [ ] Code follows style guidelines
+- [ ] Commit messages are clear
+
+### 2. Submitting PR
+
+1. Push your branch to your fork:
+   ```bash
+   git push origin feature/my-new-feature
+   ```
+
+2. Open a pull request on GitHub
+
+3. Fill in the PR template:
+   - Describe the changes
+   - Reference related issues
+   - List testing performed
+   - Add screenshots for UI changes
+
+### 3. Review Process
+
+- Maintainers will review your PR
+- Address feedback by pushing new commits
+- Once approved, maintainer will merge
+
+### 4. After Merge
+
+- Delete your feature branch
+- Pull latest changes:
+   ```bash
+   git checkout main
+   git pull upstream main
+   ```
+
+## Types of Contributions
+
+### Bug Fixes
+
+1. Check if issue already exists
+2. If not, create an issue describing the bug
+3. Reference the issue in your PR
+
+### New Features
+
+1. Discuss in an issue first (for large features)
+2. Implement the feature
+3. Add tests and documentation
+4. Submit PR
+
+### Documentation
+
+Documentation improvements are always welcome:
+- Fix typos
+- Clarify instructions
+- Add examples
+- Improve organization
+
+### Testing
+
+Help improve test coverage:
+- Add missing tests
+- Improve existing tests
+- Add integration tests
+
+## Project Structure
+
+```
+tla_visualiser/
+├── CMakeLists.txt          # Build configuration
+├── conanfile.txt           # Dependencies
+├── src/                    # C++ implementation
+├── include/                # Public headers
+├── qml/                    # QML UI files
+├── tests/                  # Unit tests
+├── examples/               # Example TLA+ specs
+├── docs/                   # Documentation
+└── .github/workflows/      # CI/CD
+```
+
+## Development Tips
+
+### Building in Debug Mode
+
+```bash
+cmake -B build-debug -G Ninja \
+    -DCMAKE_BUILD_TYPE=Debug \
+    -DCMAKE_TOOLCHAIN_FILE=build-debug/conan_toolchain.cmake
+cmake --build build-debug
+```
+
+### Running with Debugging
+
+```bash
+# GDB
+gdb ./build-debug/tla_visualiser
+
+# LLDB
+lldb ./build-debug/tla_visualiser
+```
+
+### Qt Creator
+
+Open `CMakeLists.txt` in Qt Creator for integrated development:
+- Syntax highlighting
+- Code completion
+- Visual debugging
+- QML preview
+
+### Verbose Build
+
+```bash
+cmake --build build --config Release --verbose
+```
+
+### CMake Reconfigure
+
+```bash
+cmake --build build --target rebuild_cache
+```
+
+## Getting Help
+
+- **GitHub Issues**: Report bugs or request features
+- **Discussions**: Ask questions or discuss ideas
+- **Documentation**: Check `docs/` directory
+
+## Recognition
+
+Contributors will be:
+- Listed in release notes
+- Credited in documentation
+- Acknowledged in the project
+
+Thank you for contributing to TLA+ Visualiser!
--- a/QUICKSTART.md
+++ b/QUICKSTART.md
@@ -0,0 +1,210 @@
+# Quick Start Guide
+
+Get up and running with TLA+ Visualiser in 5 minutes!
+
+## Prerequisites
+
+Make sure you have:
+- CMake 3.22+
+- Qt 6.5+
+- A C++20 compiler
+- Conan package manager
+
+See [BUILDING.md](docs/BUILDING.md) for detailed installation instructions.
+
+## Installation
+
+### Step 1: Clone and Install Dependencies
+
+```bash
+# Clone repository
+git clone https://github.com/johndoe6345789/tla_visualiser.git
+cd tla_visualiser
+
+# Install dependencies
+pip install conan
+conan profile detect
+conan install . --output-folder=build --build=missing
+```
+
+### Step 2: Build
+
+```bash
+# Configure
+cmake -B build -G Ninja \
+    -DCMAKE_BUILD_TYPE=Release \
+    -DCMAKE_TOOLCHAIN_FILE=build/conan_toolchain.cmake
+
+# Build
+cmake --build build --config Release
+```
+
+### Step 3: Run
+
+```bash
+./build/tla_visualiser
+```
+
+## First Use
+
+### 1. Import a Specification
+
+**Option A: From Examples**
+- Open the application
+- Go to: File → Import from GitHub
+- Paste: `https://github.com/tlaplus/Examples/blob/master/specifications/ewd998/EWD998.tla`
+- Click Import
+
+**Option B: Local Example**
+- Use the included example: `examples/SimpleCounter.tla`
+- Import it directly through the Import tab
+
+### 2. Run Model Checker
+
+- After importing, click "Run Model Checker"
+- Wait for TLC to complete
+- Results will appear automatically
+
+### 3. Explore Results
+
+**Graph View:**
+- Click the "Graph View" tab
+- See the state space visualized as a graph
+- Click nodes to inspect states
+
+**Trace View:**
+- Click the "Trace View" tab
+- Navigate through execution traces step-by-step
+- View variable values at each step
+
+**Invariants:**
+- Click the "Invariants" tab
+- See which invariants passed/failed
+
+### 4. Export
+
+Export your results:
+- **Graph**: File → Export Graph → SVG or PNG
+- **Trace**: File → Export Trace → JSON or Markdown
+
+## Common Workflows
+
+### Workflow 1: Explore Public TLA+ Specs
+
+```
+1. Find a TLA+ spec on GitHub
+2. Copy the URL (file or repository)
+3. Import via File → Import from GitHub
+4. Run model checker
+5. Visualize and explore
+```
+
+### Workflow 2: Analyze Your Own Specs
+
+```
+1. Create your .tla file locally
+2. Optionally create a .cfg file
+3. In TLA+ Visualiser, use Import tab
+4. Browse to your local file
+5. Run and analyze
+```
+
+### Workflow 3: Compare Runs
+
+```
+1. Run model checker on a spec
+2. File → Save Run Results
+3. Modify spec or config
+4. Run again
+5. File → Load Run Results to compare
+```
+
+## Tips & Tricks
+
+### Keyboard Shortcuts
+
+- `Ctrl+I` (Cmd+I on Mac): Import dialog
+- `Ctrl+R` (Cmd+R): Run model checker
+- `Ctrl+E` (Cmd+E): Export current view
+- `Ctrl+Q` (Cmd+Q): Quit
+
+### Performance
+
+For large state spaces:
+- Start with small models
+- Use state constraints in TLC config
+- Increase Java heap size: `export JAVA_OPTS="-Xmx4g"`
+
+### Caching
+
+Imported specs are cached in:
+- Linux/Mac: `/tmp/tla_visualiser_cache/`
+- Windows: `%TEMP%\tla_visualiser_cache\`
+
+Clear cache to force re-download:
+```bash
+rm -rf /tmp/tla_visualiser_cache/
+```
+
+## Troubleshooting
+
+### TLC Not Found
+
+Make sure TLC (tla2tools.jar) is:
+- Downloaded from https://github.com/tlaplus/tlaplus/releases
+- In your PATH or current directory
+- Accessible via `java -jar tla2tools.jar`
+
+### Qt Not Found During Build
+
+Specify Qt location:
+```bash
+export Qt6_DIR=/path/to/Qt/6.5.0/gcc_64/lib/cmake/Qt6
+cmake -B build ...
+```
+
+### Import Fails
+
+- Check internet connection
+- Verify GitHub URL is correct
+- Check GitHub rate limits (60 requests/hour without auth)
+
+### Build Errors
+
+Clean and rebuild:
+```bash
+rm -rf build
+conan install . --output-folder=build --build=missing
+cmake -B build ...
+cmake --build build
+```
+
+## Next Steps
+
+- Read the full [README](README.md)
+- Check [ARCHITECTURE](docs/ARCHITECTURE.md) for design details
+- See [CONTRIBUTING](CONTRIBUTING.md) to contribute
+- Try example specs in `examples/`
+
+## Getting Help
+
+- **Documentation**: Check `docs/` directory
+- **Issues**: https://github.com/johndoe6345789/tla_visualiser/issues
+- **Examples**: See `examples/` directory
+
+## Example Session
+
+```bash
+# Start the app
+./build/tla_visualiser
+
+# In the application:
+# 1. File → Import from GitHub
+# 2. Enter: https://github.com/tlaplus/Examples/blob/master/specifications/ewd998/EWD998.tla
+# 3. Click Import
+# 4. Click "Run Model Checker"
+# 5. Switch to "Graph View" tab
+# 6. Explore the state space!
+```
+
+Happy visualizing! 🚀
--- a/build.bat
+++ b/build.bat
@@ -0,0 +1,145 @@
+@echo off
+REM Build script for TLA+ Visualiser (Windows)
+
+setlocal enabledelayedexpansion
+
+echo ===================================
+echo TLA+ Visualiser Build Script
+echo ===================================
+echo.
+
+REM Parse arguments
+set BUILD_TYPE=Release
+set CLEAN=false
+set RUN_TESTS=true
+
+:parse_args
+if "%~1"=="" goto check_prereqs
+if "%~1"=="--debug" (
+    set BUILD_TYPE=Debug
+    shift
+    goto parse_args
+)
+if "%~1"=="--clean" (
+    set CLEAN=true
+    shift
+    goto parse_args
+)
+if "%~1"=="--no-tests" (
+    set RUN_TESTS=false
+    shift
+    goto parse_args
+)
+if "%~1"=="--help" (
+    echo Usage: build.bat [OPTIONS]
+    echo.
+    echo Options:
+    echo   --debug      Build in Debug mode ^(default: Release^)
+    echo   --clean      Clean build directory before building
+    echo   --no-tests   Skip running tests
+    echo   --help       Show this help message
+    exit /b 0
+)
+echo Unknown option: %~1
+echo Use --help for usage information
+exit /b 1
+
+:check_prereqs
+echo Checking prerequisites...
+
+where cmake >nul 2>&1
+if errorlevel 1 (
+    echo Error: cmake not found
+    exit /b 1
+)
+
+where ninja >nul 2>&1
+if errorlevel 1 (
+    echo Error: ninja not found
+    exit /b 1
+)
+
+where conan >nul 2>&1
+if errorlevel 1 (
+    echo Error: conan not found. Install with: pip install conan
+    exit /b 1
+)
+
+echo All required tools found
+echo.
+
+REM Clean if requested
+if "%CLEAN%"=="true" (
+    echo Cleaning build directory...
+    if exist build rmdir /s /q build
+    echo Clean complete
+    echo.
+)
+
+REM Detect Conan profile
+if not exist "%USERPROFILE%\.conan2" if not exist "%USERPROFILE%\.conan" (
+    echo Detecting Conan profile...
+    conan profile detect
+    echo Conan profile detected
+    echo.
+)
+
+REM Install dependencies
+echo Installing dependencies with Conan...
+conan install . --output-folder=build --build=missing
+if errorlevel 1 (
+    echo Error: Conan install failed
+    exit /b 1
+)
+echo Dependencies installed
+echo.
+
+REM Configure CMake
+echo Configuring CMake ^(%BUILD_TYPE%^)...
+cmake -B build -G Ninja ^
+    -DCMAKE_BUILD_TYPE=%BUILD_TYPE% ^
+    -DCMAKE_TOOLCHAIN_FILE=build/conan_toolchain.cmake
+if errorlevel 1 (
+    echo Error: CMake configuration failed
+    exit /b 1
+)
+echo Configuration complete
+echo.
+
+REM Build
+echo Building project...
+cmake --build build --config %BUILD_TYPE%
+if errorlevel 1 (
+    echo Error: Build failed
+    exit /b 1
+)
+echo Build complete
+echo.
+
+REM Run tests if requested
+if "%RUN_TESTS%"=="true" (
+    echo Running tests...
+    cd build
+    ctest --output-on-failure
+    if errorlevel 1 (
+        echo Some tests failed
+        cd ..
+        exit /b 1
+    )
+    echo All tests passed
+    cd ..
+    echo.
+)
+
+REM Success message
+echo ===================================
+echo Build successful!
+echo ===================================
+echo.
+echo To run the application:
+echo   build\tla_visualiser.exe
+echo.
+echo Build artifacts are in: build\
+echo Executable: build\tla_visualiser.exe
+
+endlocal
--- a/build.sh
+++ b/build.sh
@@ -0,0 +1,123 @@
+#!/bin/bash
+# Build script for TLA+ Visualiser
+
+set -e  # Exit on error
+
+echo "==================================="
+echo "TLA+ Visualiser Build Script"
+echo "==================================="
+echo
+
+# Colors for output
+GREEN='\033[0;32m'
+YELLOW='\033[1;33m'
+RED='\033[0;31m'
+NC='\033[0m' # No Color
+
+# Check for required tools
+echo "Checking prerequisites..."
+
+command -v cmake >/dev/null 2>&1 || { echo -e "${RED}Error: cmake not found${NC}"; exit 1; }
+command -v ninja >/dev/null 2>&1 || { echo -e "${RED}Error: ninja not found${NC}"; exit 1; }
+command -v conan >/dev/null 2>&1 || { echo -e "${RED}Error: conan not found. Install with: pip install conan${NC}"; exit 1; }
+
+echo -e "${GREEN}✓ All required tools found${NC}"
+echo
+
+# Parse arguments
+BUILD_TYPE="Release"
+CLEAN=false
+RUN_TESTS=true
+
+while [[ $# -gt 0 ]]; do
+    case $1 in
+        --debug)
+            BUILD_TYPE="Debug"
+            shift
+            ;;
+        --clean)
+            CLEAN=true
+            shift
+            ;;
+        --no-tests)
+            RUN_TESTS=false
+            shift
+            ;;
+        --help)
+            echo "Usage: $0 [OPTIONS]"
+            echo
+            echo "Options:"
+            echo "  --debug      Build in Debug mode (default: Release)"
+            echo "  --clean      Clean build directory before building"
+            echo "  --no-tests   Skip running tests"
+            echo "  --help       Show this help message"
+            exit 0
+            ;;
+        *)
+            echo -e "${RED}Unknown option: $1${NC}"
+            echo "Use --help for usage information"
+            exit 1
+            ;;
+    esac
+done
+
+# Clean if requested
+if [ "$CLEAN" = true ]; then
+    echo -e "${YELLOW}Cleaning build directory...${NC}"
+    rm -rf build
+    echo -e "${GREEN}✓ Clean complete${NC}"
+    echo
+fi
+
+# Detect Conan profile
+if [ ! -d "$HOME/.conan2" ] && [ ! -d "$HOME/.conan" ]; then
+    echo "Detecting Conan profile..."
+    conan profile detect
+    echo -e "${GREEN}✓ Conan profile detected${NC}"
+    echo
+fi
+
+# Install dependencies
+echo "Installing dependencies with Conan..."
+conan install . --output-folder=build --build=missing
+echo -e "${GREEN}✓ Dependencies installed${NC}"
+echo
+
+# Configure CMake
+echo "Configuring CMake ($BUILD_TYPE)..."
+cmake -B build -G Ninja \
+    -DCMAKE_BUILD_TYPE=$BUILD_TYPE \
+    -DCMAKE_TOOLCHAIN_FILE=build/conan_toolchain.cmake
+echo -e "${GREEN}✓ Configuration complete${NC}"
+echo
+
+# Build
+echo "Building project..."
+cmake --build build --config $BUILD_TYPE
+echo -e "${GREEN}✓ Build complete${NC}"
+echo
+
+# Run tests if requested
+if [ "$RUN_TESTS" = true ]; then
+    echo "Running tests..."
+    cd build
+    if ctest --output-on-failure; then
+        echo -e "${GREEN}✓ All tests passed${NC}"
+    else
+        echo -e "${RED}✗ Some tests failed${NC}"
+        exit 1
+    fi
+    cd ..
+    echo
+fi
+
+# Success message
+echo "==================================="
+echo -e "${GREEN}Build successful!${NC}"
+echo "==================================="
+echo
+echo "To run the application:"
+echo "  ./build/tla_visualiser"
+echo
+echo "Build artifacts are in: build/"
+echo "Executable: build/tla_visualiser"
--- a/examples/README.md
+++ b/examples/README.md
@@ -0,0 +1,32 @@
+# Example TLA+ Specifications
+
+This directory contains example TLA+ specifications for testing and demonstrating TLA+ Visualiser.
+
+## SimpleCounter.tla
+
+A basic counter specification that demonstrates:
+- Simple state variables
+- Increment/Decrement actions
+- Type invariants
+
+### Usage
+
+1. Import the spec in TLA+ Visualiser
+2. Run the model checker
+3. Explore the state graph (will show counter incrementing/decrementing)
+
+### With Command Line TLC
+
+If you have TLC installed:
+
+```bash
+java -jar tla2tools.jar SimpleCounter.tla -config SimpleCounter.cfg
+```
+
+## Adding More Examples
+
+Feel free to add more example specs to demonstrate various TLA+ features:
+- Concurrent algorithms
+- Distributed systems
+- Safety/liveness properties
+- Deadlock detection
--- a/examples/SimpleCounter.cfg
+++ b/examples/SimpleCounter.cfg
@@ -0,0 +1,2 @@
+SPECIFICATION Spec
+INVARIANT TypeInvariant
--- a/examples/SimpleCounter.tla
+++ b/examples/SimpleCounter.tla
@@ -0,0 +1,20 @@
+---------------------------- MODULE SimpleCounter ----------------------------
+(* A simple counter specification for testing TLA+ Visualiser *)
+
+EXTENDS Naturals
+
+VARIABLE counter
+
+Init == counter = 0
+
+Increment == counter' = counter + 1
+
+Decrement == counter' = counter - 1
+
+Next == Increment \/ Decrement
+
+Spec == Init /\ [][Next]_counter
+
+TypeInvariant == counter \in Nat
+
+=============================================================================
--- a/tests/test_tlc_runner.cpp
+++ b/tests/test_tlc_runner.cpp
@@ -1,4 +1,6 @@
 #include <QtTest/QtTest>
+#include <QDir>
+#include <QFile>
 #include "tlc_runner.h"

 class TestTLCRunner : public QObject