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 User Guide

C2PO User Guide#

  • Input Language
    • Identifiers
    • Types
    • Inputs
    • Supported Operators
      • Set Aggregation
    • Definitions
    • Specifications
      • Specification Labels
      • Assume-Guarantee Contracts
    • Atomic Checkers
  • Signal Mapping
    • Map File
    • Trace File
  • MLTL Standard Format
  • Optimizations
    • Common Sub-expression Elimination
    • Rewrite Rules
    • Equality Saturation
    • Extended Operators
  • Output Formats
  • CLI Options
    • Positional Arguments:
    • Optional Arguments:

previous

Runtime Monitoring

next

Input Language

By Laboratory for Temporal Logic

© Copyright 2023, Laboratory for Temporal Logic.