temex

temex - 用于评估随时间变化的系统的正则表达式样式的时态表达式

该库实现了temexes，这是一种结合命题逻辑公式和正则表达式运算符的结构，旨在提供一种简单易用的时态逻辑。

目录

1. 简介
2. 概述
3. Temex语法
   • 命题公式语法
   • 正则表达式运算符语法
4. 支持的跟踪格式
5. 使用方法
6. 示例
   • 示例 1：使用is_match在polars DataFrame中测试匹配
   • 示例 2：使用find查找匹配的位置
   • 示例 3：使用find_iter查找所有非重叠匹配
7. 许可证

简介

时态逻辑在计算机科学内外有许多有用的应用。详细的讨论超出了本文件的范畴，但有关良好的介绍可在此处找到。尽管时态逻辑有许多用例，但大多数实现某种形式时态逻辑的工具都是为形式方法专家和逻辑学家设计的，而不是为普通大众设计。因此，它们可能对门外汉来说显得晦涩难懂。

temex的目的在于提供一个简单的工具，允许普通软件工程师和数据分析师利用时态逻辑的力量。它设计得易于理解和使用，只需要基本的命题逻辑和正则表达式知识。

概述

真值赋值 是布尔变量到真值（即，true 或 false）的映射。当命题逻辑公式中出现的所有布尔变量都被赋予一个值时，那么该公式评估为 true 或 false。我们可以将公式视为定义一组真值赋值：即，使该公式评估为 true 的真值赋值。

正则表达式要么是字符，要么是子表达式通过正则表达式运算符连接的复合表达式。正则表达式定义了一组字符序列：与正则表达式匹配的序列。

我们可以将真值赋值视为字符，将命题公式视为一个正则表达式，其中它定义的真值赋值通过交替连接（即正则表达式运算符 |）。例如，公式 not (p and q) 可以看作是 {p = true, q = false} | {p = false, q = true} | {p = false, q = false}。

如果我们把真值赋值看作字符，把命题公式看作这些字符的交替，那么如果我们用正则表达式运算符连接命题公式，并根据正则表达式的普通语义来解释结果，我们就会得到一个定义真值赋值序列的东西。我们称之为 temex，即时间表达式。

我们可以使用 temex 来搜索真值赋值序列（以下简称为 轨迹），就像我们可以使用正则表达式来搜索字符串一样。 temex 实现了这一功能。

Temex语法

Temex 原子是方括号内（[ 和 ]）的命题公式。它们可以用正则表达式运算符连接，就像字符可以用正则表达式运算符连接一样。

命题公式语法

命题公式可能是一个布尔变量（以字母字符开头，可能包含字母、数字以及下划线），或者是一个复合公式，其中子公式通过命题连接词连接。 temex 使用英文单词 not、and 和 or 分别表示否定、合取和析取；not 的运算符优先级最高，而 and 和 or 的运算符优先级相等且是右结合的。示例

• f123
• is_sunny and not is_raining
• cpu_GT_80 and not(mem_LT_40 or io_LT_20)

正则表达式运算符语法

temex 的正则表达式运算符继承了 regex crate 的语法，temex 使用它来实现其正则表达式运算符。

在以下形式中，phi、phi_1 和 phi_2 是命题公式，而 n 和 m 是自然数

[phi_1][phi_2]      concatenation (phi_1 followed by phi_2)
[phi_1]|[phi_2]     alternation (phi_1 or phi_2, prefer phi_1)
[phi]*              zero or more of phi (greedy)
[phi]+              one or more of phi (greedy)
[phi]?              zero or one of phi (greedy)
[phi]*?             zero or more of phi (ungreedy/lazy)
[phi]+?             one or more of phi (ungreedy/lazy)
[phi]??             zero or one of phi (ungreedy/lazy)
[phi]{n,m}          at least n phi and at most m phi (greedy)
[phi]{n,}           at least n phi (greedy)
[phi]{n}            exactly n phi
[phi]{n,m}?         at least n phi and at most m phi (ungreedy/lazy)
[phi]{n,}?          at least n phi (ungreedy/lazy)
[phi]{n}?           exactly n phi

支持的跟踪格式

以下轨迹格式受支持

• polars 数据帧，其中所有列都是布尔值。列名被解释为布尔变量的名称，数据帧的行被解释为真值赋值。

• 编码为 UTF8 字符串或文件的 CSV 文件。第一行应包含布尔变量的名称，接下来的行应包含 1 或 0 的值，分别对应于 true 或 false。标题之后的行被解释为真值赋值。

在匹配跟踪时，temex模式中的变量名和跟踪中的变量名必须相同；如果跟踪中有额外的变量，则搜索将导致错误。

使用方法

在执行任何搜索操作之前，temex模式和跟踪必须进行编译。编译temex模式使用Temex::new，而编译跟踪使用TemexTrace::try_from。可以使用temex的方法执行搜索；完整的列表在这里。

示例

示例 1：使用is_match在polars DataFrame中测试匹配

以下示例展示了如何在polars DataFrame中执行temex搜索。在搜索之前，DataFrame必须转换为TemexTrace。示例还展示了如何将TemexTrace转换回DataFrame。注意使用^和$，它们是分别匹配跟踪开始和结束的锚点。

use polars::df;
use polars::prelude::*;
use temex::{Temex, TemexTrace};
let df = df! [
    "p1" => [true, true, true],
    "p2" => [false, false, false],
    "p3" => [true, false, true]
]
.unwrap();
let trace = TemexTrace::try_from(df.clone()).unwrap();
let te = Temex::new("^[p1 and (p2 or p3)][p1][p1 or p2 and not p3]$").unwrap();

assert!(te.is_match(&trace).unwrap());

// We can convert the TemexTrace back to a DataFrame
let df_from_trace = polars::frame::DataFrame::try_from(trace).unwrap();
assert_eq!(df, df_from_trace);

示例 2：使用find查找匹配的位置

在这里，我们使用find方法找到跟踪中最左侧第一个匹配的范围。

let trace_str = "CPU_core1_GT_80, CPU_core2_GT_80, mem_usage_GT_40\n\
                       0,               0,               0\n\
                       1,               0,               0\n\
                       0,               1,               0\n\
                       0,               0,               1\n\
                       1,               0,               1\n\
                       0,               1,               1\n\
                       1,               1,               0\n\
                       1,               1,               0\n\
                       1,               1,               0\n";

let trace = trace_str.parse::<TemexTrace>().unwrap();
let te = Temex::new("[CPU_core1_GT_80 and CPU_core2_GT_80 and not mem_usage_GT_40]+").unwrap();

assert_eq!(te.find(&trace).unwrap().unwrap().range(), 6..9);

示例 3：使用find_iter查找所有非重叠匹配

在这个示例中，我们展示了如何使用find_iter方法在跟踪中找到多个非重叠匹配。

let trace_str = "is_sunny, is_windy\n\
                        1,        0\n\
                        1,        0\n\
                        1,        0\n\
                        0,        0\n\
                        1,        0\n\
                        1,        0\n\
                        1,        0\n\
                        1,        1\n\
                        1,        0\n\
                        1,        0\n\
                        1,        0\n";

let trace = TemexTrace::try_from(trace_str).unwrap();
let te = Temex::new("[is_sunny and not is_windy]{3}").unwrap();

for te_match in te.find_iter(&trace) {
    println!("{:?}", te_match.range());
}

// Output:
// 0..3
// 4..7
// 8..11

许可证

版权（c）2023 Kevin Wayne Smith

此项目根据您的选择受以下之一许可：

• Apache License, Version 2.0 (https://apache.ac.cn/licenses/LICENSE-2.0)

• MIT License (https://opensource.org/licenses/MIT)

。