时间戳

首页 > 解决方案 > 使用 CrossHair 区分自动机和 python 函数

python - 使用 CrossHair 区分自动机和 python 函数

问题描述

我有一个定义语言的函数，让我们调用 L，这个函数获取一个单词并返回 True 或 False。

我还有一个确定性有限 autumata，它假设接受语言中的单词并后悔语言 L 中没有的单词。

我的任务是获得一个能够区分 dfa 和 python 函数的反例。

我想知道 CrossHair 是否对这项任务有用。

我期待类似的东西：

counterexmaple = checker(dfa, func)

谢谢

标签： pythonsolverfinite-automatamodel-checking

解决方案

概括

您或许可以使用CrossHair来解决此类问题。但是，执行确定性有限自动机 (DFA) 将涉及很多分支行为，并且 CrossHair 在这种情况下表现不佳。在大多数情况下，您最好使用带有假设的随机测试方法。我将描述这两种方法。

预赛

首先，您希望能够在 python 中表达您的 DFA 以比较实现。这是一个例子：

from typing import Tuple, Dict

# We construct a DFA that accepts any string that ends                                                                                                                        
# with "abc":                                                                                                                                                                 
_TRANSITION_TABLE: Dict[Tuple[int, str], int] = {
    # state #0: we have not yet seen "a" (initial state)                                                                                                                      
    (0, 'a'): 1,
    # state #1: we've seen "a"                                                                                                                                                
    (1, 'a'): 1,
    (1, 'b'): 2,
    # state #2: we've seen "ab"                                                                                                                                               
    (2, 'a'): 1,
    (2, 'c'): 3,
    # state #3: we've seen "abc" (final state)                                                                                                                                
    (3, 'a'): 1,
}

def dfa_checker(s: str) -> bool:
    state = 0
    for char in s:
        state = _TRANSITION_TABLE.get((state, char), 0)
    return state == 3

def correct_custom_checker(s: str) -> bool:
    return s.endswith("abc")

def incorrect_custom_checker(s: str) -> bool:
    return s.endswith("bc")

十字线解决方案

您可以给自定义实现一个合同，声明其结果与 DFA 相同：

def incorrect_custom_checker(s: str) -> bool:
    ''' post: __return__ == dfa_checker(s) '''
    return bool(re.fullmatch('[abc]*', s) and s.endswith("bc"))

虽然实际功能不需要，但为我们的字母表 (abc) 添加正则表达式有助于 CrossHair 找到解决方案。现在我们可以让 CrossHair 尝试反驳合同：

$ crosshair check example.py
example.py:29:error:false when calling incorrect_custom_checker(s = 'bc') (which returns True)

它找到了反例“bc”，它被不正确的_custom_checker() 接受但被 DFA 拒绝。

此外，还有一个非常新的、基本上未记录的十字准线命令，使这类事情变得更加容易。您可以使用以下方法比较任意两个任意 python 函数：

$ crosshair diffbehavior example.incorrect_custom_checker example.dfa_checker
  given: (s='bc')
- returns: True
+ returns: False

如果您需要完全以编程方式执行此操作，您可以在此处访问执行此操作的 CrossHair 内部。随着 CrossHair 代码库的发展，这种方法将失效，但为了完整起见，我将其包含在此处。

假设解

正如我之前提到的那样，进行大量随机测试可能对您更有效。这是一种在假设中做到这一点的方法：

import hypothesis
from hypothesis.strategies import text
@hypothesis.given(text(alphabet="abc"))
def test_checkers_equivalent(s: str) -> None:
    assert dfa_checker(s) == incorrect_custom_checker(s)

运行pytest example.py会发现相同的“bc”反例。

推荐阅读