Skip to content
New issue

Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.

Sign up for GitHub

By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.

Already on GitHub? Sign in to your account

Jump to bottom

a question about PTS #214

Open
yin99 opened this issue Nov 15, 2023 · 6 comments
Open

a question about PTS #214

yin99 opened this issue Nov 15, 2023 · 6 comments

Comments

@yin99
Copy link

yin99 commented Nov 15, 2023

I hava read the paper LTSmin: High-Performance Language-Independent Model Checking.
In this paper, it said A PTS is a structure P = 〈SP , →P , s0, L〉 and s0 = 〈s01, . . . , s0 N 〉 ∈ SP is the initial state.
Does this mean that the initial state of the model detected by ltsmin is a certain state ？Or can this initial state be a set of states?
@jacopol
Copy link
Contributor

jacopol commented Nov 15, 2023 via email

@yin99
Copy link
Author

yin99 commented Nov 16, 2023

Hi, a state space in LTSmin has a unique initial state. You can add a “pseudo” initial state with nondeterministic transitions to the desired initial states, when needed. Kind regards, Jaco van de Pol Verzonden vanuit Outlook voor iOShttps://aka.ms/o0ukef
…
________________________________ Van: yin99 @.> Verzonden: Wednesday, November 15, 2023 3:49:25 AM Aan: utwente-fmt/ltsmin @.> CC: Subscribed @.> Onderwerp: [utwente-fmt/ltsmin] a question about PTS (Issue #214) I hava read the paper LTSmin: High-Performance Language-Independent Model Checking. In this paper, it said A PTS is a structure P = 〈SP , →P , s0, L〉 and s0 = 〈s01, . . . , s0 N 〉 ∈ SP is the initial state. Does this mean that the initial state of the model detected by ltsmin is a certain state ？Or can this initial state be a set of states? — Reply to this email directly, view it on GitHub<#214>, or unsubscribehttps://github.com/notifications/unsubscribe-auth/ABTGAZN2F37L2R543KZE3LTYEQUTLAVCNFSM6AAAAAA7LZNVFKVHI2DSMVQWIX3LMV43ASLTON2WKOZRHE4TGOJTGMYDEOI. You are receiving this because you are subscribed to this thread.Message ID: @.>

Thanks for your answer. And there are some related questions about PTS.

Firstly, PTS said Sp = S1×...×SN. In my understanding, N refers to the dimension N of a state s, so S1... SN represents the set of values on the corresponding dimension of state s, for example, S1 is the set of values for x1. I would like to ask if my understanding is incorrect.

Secondly, Does PTS allow a state in the model to have multiple successor states? K migration groups refer to K different successor groups in a state. Or is it possible to divide the entire state space of the state machine into K groups? I don't quite understand how to determine the value of K in a state machine. Looking forward to your reply。

@jacopol
Copy link
Contributor

jacopol commented Nov 16, 2023 via email

@yin99
Copy link
Author

yin99 commented Nov 16, 2023

Indeed, N is the dimension of the state space, so every state consists of a vector of length N (internally represented by N integers). The transitions are also structured, where the partition relation is the union of K transition groups. In principle, each transition group can still be non-deterministic, and different partition groups can overlap. The transition groups are supposed to reflect the structure of the specification, i.e., bundle transition steps that are there for the same reason. It is up to the modeling language module to decide what the partition groups are. For instance, in Petri Nets, a partition group corresponds with a Petri-net transition, in Process Algebra, it could correspond with a particular (synchronization) action, in Promela it could be a statement, or a block of statements, etc. Hope this clarifies the definitions,

Thanks,

I would like to use an example to express my confusion.

If there is a simple automaton with only two variables a and b. I define his migration rules as follows.
State machine can translate from state s=(a，b) to state t=(a‘，b'） iff (a | b) | (a '| b')=TRUE.

It is obvious that the following conclusion can be drawn:

The state machine has a total of four states (0,0), (0,1), (1,0), and (1,1)

It is feasible to transfer any state to several other states, and all three states except state (0,0) can be transferred to themselves.

So in this example, what is K?

Is K 1? Because there is only one translation rule.
Or is K 2? Because (0,0) can only translate to three states, while the other three states can translate to four states.

@jacopol
Copy link
Contributor

jacopol commented Nov 16, 2023 via email

@yin99
Copy link
Author

yin99 commented Nov 20, 2023

Hi, in such cases, K cannot be derived from the automaton, you will have to define (and choose) a K, typically depending from a high level specification. For instance, you could have two “firing” rules (modifying your example): 1: (a,b) -> (not a, b) 2: (a,b) -> (a, not b) In this case, K=2. The first transition group contains concrete transitions (0,0)->(1,0), (0,1)->(1,1), (1,0)->(0,0), (1,1)->(0,1) The second transition group contains concrete transitions (0,0)->(0,1), (1,0)->(1,1), (0,1)->(0,0), (1,1)->(1,0) But you could also specify a transition system with exactly these 8 concrete transitions by a specification with K=1 or K=4 “symbolic” transition (groups), for instance. Kind regards, Jaco van de Pol
…
-- Jaco van de Pol, Professor of Computer Science Aarhus University & University of Twente From: yin99 @.> Sent: Thursday, November 16, 2023 10:25 AM To: utwente-fmt/ltsmin @.> Cc: Jaco van de Pol @.>; Comment @.> Subject: Re: [utwente-fmt/ltsmin] a question about PTS (Issue #214) Indeed, N is the dimension of the state space, so every state consists of a vector of length N (internally represented by N integers). The transitions are also structured, where the partition relation is the union of K transition groups. In principle, each transition group can still be non-deterministic, and different partition groups can overlap. The transition groups are supposed to reflect the structure of the specification, i.e., bundle transition steps that are there for the same reason. It is up to the modeling language module to decide what the partition groups are. For instance, in Petri Nets, a partition group corresponds with a Petri-net transition, in Process Algebra, it could correspond with a particular (synchronization) action, in Promela it could be a statement, or a block of statements, etc. Hope this clarifies the definitions, Thanks, I would like to use an example to express my confusion. If there is a simple automaton with only two variables a and b. I define his migration rules as follows. State machine can translate from state s=(a，b) to state t=(a‘，b'） iff (a | b) | (a '| b')=TRUE. It is obvious that the following conclusion can be drawn: The state machine has a total of four states (0,0), (0,1), (1,0), and (1,1) It is feasible to transfer any state to several other states, and all three states except state (0,0) can be transferred to themselves. So in this example, what is K? Is K 1? Because there is only one translation rule. Or is K 2? Because (0,0) can only translate to three states, while the other three states can translate to four states. — Reply to this email directly, view it on GitHub<#214 (comment)>, or unsubscribehttps://github.com/notifications/unsubscribe-auth/ABTGAZNDPACNTNRT5JH4H5TYEXLWZAVCNFSM6AAAAAA7LZNVFKVHI2DSMVQWIX3LMV43OSLTON2WKQ3PNVWWK3TUHMYTQMJUGA3TENZYGU. You are receiving this because you commented.Message ID: @.@.>>

I have read the source of LTSmin, but I still don't understand the difference between next_state and next_action.
They both set a method for type next_method_grey_t. What is the difference between them.

Besides,function pointer of type next_method_grey_t has 5 param and returns the number of new transitions found.Will the function of t return the number of next states for the current state of the input?

Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment
Assignees
No one assigned
Labels
None yet
Projects
None yet
Milestone
No milestone
Development

No branches or pull requests
2 participants
@jacopol @yin99