UPPAAL에서 시계의 현재 값을 얻고이를 정수 변수에 저장하는 방법은 무엇입니까?

Question

누구나 clock 변수의 현재 값을 얻고 정수 변수에 저장하는 방법을 알려줄 수 있습니까? 나는 k = t (k는 정수이고 t는 시계)를 시도했지만 "호환되지 않는 유형 오류"가 발생합니다. 또한 k = (int) t 시도했지만 "예기치 않은 T_INT"문법 오류가 발생합니다.

클럭의 현재 값을 가져 와서 변수에 저장하기 위해 UPPAAL의 클럭에 사용할 수있는 형식 변환이 있습니까? ?

Answer 1

시간은 (상징적으로) 처리되기 때문에 불가능합니다. UPPAAL 시뮬레이터를 사용하면 시계 값이 구체적으로 표시되지 않고 시계 제한으로 표시됩니다. 따라서 시계가 어떤 가치가 있다고 말할 수는 없지만 여러 가지 제약 조건을 충족하는 현재 시계 평가가 있으므로 시계가 일정한 간격을두고 있습니다. 당신이 시계가 도달 할 수있는 최대 값을 알고 싶다면 당신은 그러나 변수를

을 정수하기 위해 시계를 비교할 수 있습니다

• :

  당신은 당신이 달성 할 수 있도록 몇 가지 관련 포인터를 원하는 지정하지 , "sup : clock"쿼리를 사용할 수 있습니다.