formal-methods

1열

1답변

SPIN 모델 검사기에서 최대 검색 깊이를 너무 작게 해결하는 방법은 무엇입니까? 가능한 이유는 무엇입니까?

내 모델 검증을하는 동안 나는이 오류를 얻고있다 는 컴파일 문자열 tesTdma.pml -a 스핀 최대 검색 깊이가 너무 작고, 깊이 = 9999 주 I입니다 이 오류의 원인을 이해하지 못합니다. 나요 누군가가 1.1.4과 SPIN 버전이 사용 ISPIN 건너 온 6.4.7

1열

1답변

공식적인 방법 : [] <> TLA에서 무한 자주 (항상 최후에)

TLA에서의 나의 이해에서, 최종 행동 (<>)은 다음 상태에서 말더듬이가 일어나는 것을 허용하지 않습니다. 그러면 무한히 자주 ([] <>)의 경우 다음 상태 변수가 더듬는 것이 허용되지 않는다는 뜻입니까? 기상 조건의 예를 들어 보면, 무한히 자주 1 년 내에 여러 날 (우리는 언제 일어날 지 모릅니다)으로 설명 될 수 있지만 비가 내리고 비가 오는 날

1열

1답변

꺾쇠 괄호 <>는 무엇을 의미합니까?

예 1 forall x,y in set {1,…,5} & X <> y => not m.temps(x) = m.temps(y) 예 2 exists i,j in set inds m.temps & i <> j and m.temps(i) > 400 and m.temps(j) > 400 <> 그 문장에서 무엇을 의미합니까?

1열

1답변

유형 클래스가 약식으로 작동하지 못함

약식으로 유형 클래스 사용을 트리거하는 방법을 이해하는 데 문제가 있습니다. section the_section structure toto [class] (A : Type) := (rel : A → A → Prop) (Hall : ∀ a, rel a a) definition P A := exists (a : A), forall x, x = a par

1열

4답변

람다 미적분학의 변수 집합이 일반적으로 무한 계산 가능으로 정의되는 이유는 무엇입니까?

람다 미적분학의 정식 설명을 읽을 때, 변수 세트는 항상 무한대로 정의되는 것으로 보입니다. 이 세트가 유한 할 수없는 이유는 분명합니다. 변수 세트를 유한으로 정의하면 용인 될 수없는 방식으로 용어 구조가 제한됩니다. 그러나 세트가 무한대로 무한하게 허용하지 않는 이유는 무엇입니까? 현재 내가받은이 질문에 대한 가장 분별있는 대답은 셀 수없이 무한한 변수

2열

1답변

상태 공간이 일부 시스템의 동작에 대한 공식적인 사양이라고 말할 수 있습니까?

시스템과 전체 상태 공간이 주어지면 그 상태 공간이 해당 시스템의 동작에 대한 공식 사양인지 말할 수 있습니까?

2열

2답변

알고리즘의 정확성을 입증하십시오.

누구든지이 질문에 답할 수 있는지 궁금합니다. 이전 시험지에서 나온 것으로 이번 해의 시험 준비를 알면됩니다. 이 질문은 너무 간단해서 완전히 잃어 버렸습니다. 정확히 무엇을 요구하고 있습니까? 최대 값을 찾으려면 다음 알고리즘을 사용하고 있습니까? {P: x≥0 ∧ y≥0 ∧ z≥0 } if (x > y && x > z) max = x; else i

1열

1답변

UPPAAL의 상태 공간 폭발

UPPAAL에서 두 플립 플롭의 시간 모델을 모델링했습니다. 몇 가지 속성을 확인하려고했는데 6M 상태에 도달했고 노트북이 RAM에서 빠져 나왔습니다. 약 5Go가 소비되었고 누군가가 무엇을 말할 수 있습니까? UPPAAL이 처리 할 수있는 대략적인 주 번호입니까? UPPAAL에서 주 폭발을 다루기위한 가능한 기술은 무엇입니까? 당신에게

3열

1답변

루프 불변과 (<a href="http://en.wikipedia.org/wiki/Predicate_transformer_semantics" rel="nofollow">http://en.wikipedia.org/wiki/Predicate_transformer_semantics</a>에서) 루프 의 약한 전제 조건을 생산하는 좋은 방법 불변 루프, 위키 백과의 목록을 감안할 때 약한 전제 조건

사이의 관계 란 : wp(while E inv I do S, R) = I \wedge \forall y. ((E \wedge I) \implies wp(S,I \wedge x < y))[x <- y] \wedge \forall y. ((\neg E \wedge I) \implies R)[x <- y] where y is a tu

1열

1답변

데이빗 사양 : 촉진 및 작업을 하나 이상의 스키마

을 적용 나는 Data 스키마의 순서를 추적 Array 스키마를 가지고있다. 프로모션을 사용하여 Array과 (과) 함께 사용할 수있는 Increment 작업을 승격 할 수 있습니다. ArrayIncrement은 Array 안에 하나의 데이터 만 씩 증가시킵니다. 어떻게하면 마다Data을 \ran data 단위로 증가 시키나요?