a question about PTS

[yin99]

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]

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 iOS<https://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 unsubscribe<https://github.com/notifications/unsubscribe-auth/ABTGAZN2F37L2R543KZE3LTYEQUTLAVCNFSM6AAAAAA7LZNVFKVHI2DSMVQWIX3LMV43ASLTON2WKOZRHE4TGOJTGMYDEOI>. You are receiving this because you are subscribed to this thread.Message ID: ***@***.***>

[yin99]

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]

Hi, 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, Jaco van de Pol

…

-- Jaco van de Pol, Professor of Computer Science Aarhus University & University of Twente From: yin99 ***@***.***> Sent: Thursday, November 16, 2023 9:30 AM To: utwente-fmt/ltsmin ***@***.***> Cc: Jaco van de Pol ***@***.***>; Comment ***@***.***> Subject: Re: [utwente-fmt/ltsmin] a question about PTS (Issue #214) 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<#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<#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。 — Reply to this email directly, view it on GitHub<#214 (comment)>, or unsubscribe<https://github.com/notifications/unsubscribe-auth/ABTGAZJGD3K3OOOISLUXY3TYEXFHRAVCNFSM6AAAAAA7LZNVFKVHI2DSMVQWIX3LMV43OSLTON2WKQ3PNVWWK3TUHMYTQMJTHE4TEMRVGY>. You are receiving this because you commented.Message ID: ***@***.******@***.***>>

[yin99]

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]

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 unsubscribe<https://github.com/notifications/unsubscribe-auth/ABTGAZNDPACNTNRT5JH4H5TYEXLWZAVCNFSM6AAAAAA7LZNVFKVHI2DSMVQWIX3LMV43OSLTON2WKQ3PNVWWK3TUHMYTQMJUGA3TENZYGU>. You are receiving this because you commented.Message ID: ***@***.******@***.***>>

[yin99]

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?