Skip to main content
Ctrl+K
R2U2 Documentation - Home R2U2 Documentation - Home
  • Quick-Start Guide
  • Installation
  • Project Structure

✏️ MLTL Monitoring

  • Specification Writing
  • Mission-time Linear Temporal Logic
  • Runtime Monitoring

📚 User Guides

  • C2PO User Guide
    • Input Language
    • Signal Mapping
    • MLTL Standard Format
    • Optimizations
    • Output Formats
    • CLI Options
  • R2U2 C Monitor User Guide
    • Building
    • Running
    • Embedding
    • Output
    • Multi-monitor
    • Configuration
  • Test Suite
  • Examples
    • Assume-Guarantee Contract Example
    • Simple Example

🛠 Developer Guides

  • C2PO Developer Guide
    • Internal Architecture
    • Parser
    • C2PO Parse Tree
    • R2U2 Front End Selection
    • Assembler
    • Testing
  • R2U2 C Monitor Developer Guide
    • Architecture
    • Internals
    • Memory Controllers
    • Execution Engines
    • Implementation
    • Debug
    • Testing
  • R2U2 Documentation
  • Contributing to R2U2

📖 References

  • File Formats
    • C2PO Input Files [.c2po]
    • MLTL Formula Files [.mltl]
    • R2U2 Assembly [.asm]
    • R2U2 Configuration Binary Files [.bin]
    • Signal Map Files [.map]
    • Signal Trace Files [.csv]
  • MLTL Grammar
  • Publications
  • .md

C2PO Developer Guide

C2PO Developer Guide#

  • Internal Architecture
    • Passes
    • Serialization
  • Parser
  • C2PO Parse Tree
    • DUOQ Sizing
    • R2U2 Engines
  • R2U2 Front End Selection
    • Booleanizer
    • Atomic Checkers
      • Available Filters:
  • Assembler
  • Testing
    • Usage
    • Configuration

previous

Simple Example

next

Internal Architecture

By Laboratory for Temporal Logic

© Copyright 2023, Laboratory for Temporal Logic.