DdManager에는 x, y, x', y'의 변수가 있고 BDD는 x 및 y으로 구성되어 있다고 가정합니다. 이제 x을 x', y에서 y'으로 변경하고 싶습니다. 즉, x' 및 y'으로 작성된 동일한 BDD를 가져 오십시오.BDD의 일부 변수를 CUDD 패키지로 바꾸려면 어떻게합니까?
CUDD 패키지를 사용하여 어떻게 얻을 수 있습니까? 모델 검사 알고리즘을 구현할 때이 문제가 발생했습니다. 이 작업을 구현하는 방법을 알고 싶거나 내가 심볼릭 모델 검사 알고리즘을 오해하고 있는지 알고 싶습니다. 대단히 감사합니다!
이 작업은 Cudd_bddSwapVariables 함수로 수행합니다. 그것은 다음과 같은 매개 변수를 가져옵니다
Cudd_bddNewVar 돌아올 것이다 BDD 노드로 표시) 변수의 첫 번째 배열 변수의 개수가 교환되는배열을 할당하고 해제해야합니다. package dd에 포함 된 CUDD의 사이 썬 바인딩을 사용하여 변수 치환의
예 :
from dd import cudd
bdd = cudd.BDD() # instantiate a shared BDD manager
bdd.declare("x", "y", "x'", "y'")
u = bdd.add_expr("x \/ y") # create the BDD for the disjunction of x and y
rename = dict(x="x'", y="y'")
v = bdd.let(rename, u) # substitution of x' for x and y' for y
s = bdd.to_expr(v)
>>> s
"ite(x', TRUE, y')"
# another way to confirm the result is as expected
v_ = bdd.add_expr("x' \/ y'")
assert v == v_
당신의 응답을 주셔서 감사합니다! 나는이 문서를 읽었지만이 기능을 전에 시도했지만 실패했다. 귀하의 답변을 읽은 후에, 나는 다시 시도하고 성공합니다. 어쩌면 이전에 잘못된 매개 변수를 설정했을 수도 있습니다. 고마워 ~ – HelloWorld