합금 모델이 너무 추상적 일 때, 추상적이지 않은 경우는 언제입니까?

Question

my last Stack Overflow post 나는 백 슬래시가 쉼표를 벗어나지 않는다면 모든 백 슬래시가 다른 백 슬래시에 의해 이스케이프되도록 제한하는 합금 모델을 만드는 방법을 묻습니다. 다니엘 잭슨이 제 게시물에 대답하여 제 모델이 더 추상적이어야한다고 제안했습니다. 사실, 나는 더 추상적 인 모델을 만들었다. 그러나 너무 추상적이어서 백 슬래시를 적절하게 제한하는 문제를 피하고 있습니다 (this post 참조).

필자는 너무 추상적 인 합금 모델이 너무 추상적 일 때 당혹 스럽다.

Answer 1

먼저 모델에 기본 세계 모델이 지나치게 복잡하게 표시되어 있다고 생각합니다. 나는 당신이 일하려고하는 문제를 알아 차리고 도주합니다. 그리고 그것은 확실히 더러운 지역입니다.

나를위한 열쇠는 Char의 순서이기 때문에 모델 사용 seq을 만드는 것입니다.

abstract sig Char {} 
    abstract sig EscapedCharacter extends Char {} 
one sig A,B,C extends Char {} 
one sig Backslash, Comma extends EscapedCharacter {} 

pred valid[ string : seq Char ] { 
    string.isEmpty 
    or 
     string[0] = Backslash 
      implies { 
       # string > 1 
      and string[1] in EscapedCharacter 
      and valid[ string.subseq[2,#string]] 
       } 
      else string[0] != Comma and valid[ string.rest ]  
} 

run valid for 4 

불행히도 이것은 재귀를 사용합니다. 재귀없이 이것을 지정할 수있는 방법은 실제로 실패합니다.하지만 찾으려고합니다. 메뉴에서 재귀를 활성화해야하기 때문에 이것은 불행한 일입니다. 이것은 3 단계로 제한되어 있습니다. 이는 작은 문제조차도 낮은 수준으로 나타납니다. 이 제한의 이유는 상태 공간을 폭발시키는 재귀가 전개되어야한다는 것입니다. 그러나 대부분의 개발자에게는 가독성이 매우 높기 때문에 재귀를 일류 시민으로 만들기위한 방법을 찾길 바랍니다. 우리는 몇 가지 예 주장 할 때 작동처럼

어쨌든, 보이는 : 쉼표 항상에 있던 원래의 요구 사항에 놓친

assert InvalidExample { 
    not valid[ 0->Backslash ] 
} 
check InvalidExample for 4 

assert InvalidExample2 { 
    not valid[ (0->A) + (1->Backslash) + (2->Backslash)+ (3->Comma) ] 
} 
check InvalidExample2 for 4 

assert ValidExample { 
    valid[ (0->Backslash) + (1->Comma) ] 
} 
check ValidExample for 4 

업데이트는 앞에 백 슬래시를 (내가 대신 내 상식을 적용)