Converting double to integer using fint() is not working. Is there any alternative for this?

[NITISH YADAV]

I want to convert 1.8 to 2.0 and then change the type of the result to an integer value. To do this, i execute the following function for the shown template.

int xx;
double dx=round(1.8);
void cast() { xx = fint(dx); }

Upon execution, the value of xx is 0. Could someone please help me figure this out.

[Marius Mikucionis]

Hi,

Floating point operations are supported only in SMC queries as it is an SMC feature:

Best regards,
Marius

The information contained in this electronic communication is intended solely for the individual(s) or entity to which it is addressed. It may contain proprietary, confidential and/or legally privileged information. Any review, retransmission, dissemination, printing, copying or other use of, or taking any action in reliance on the contents of this information by person(s) or entities other than the intended recipient is strictly prohibited and may be unlawful. If you have received this communication in error, please notify us by responding to this email or telephone and immediately and permanently delete all copies of this message and any attachments from your system(s). The contents of this message do not necessarily represent the views or policies of BITS Pilani.
--
You received this message because you are subscribed to the Google Groups "UPPAAL" group.
To unsubscribe from this group and stop receiving emails from it, send an email to uppaal+un...@googlegroups.com.
To view this discussion on the web visit https://groups.google.com/d/msgid/uppaal/a8a38093-dba2-4630-9348-07f6ac45663bn%40googlegroups.com.

[NITISH YADAV]

Suppose, i want to calculate the probability of reaching B from A, and the transitions taken from A to B includes the transition that has cast() function. What would the SMC query be like to do this?

[Marius Mikučionis]

On Monday, 19 September 2022 at 08:53:55 UTC+2:

Suppose, i want to calculate the probability of reaching B from A, and the transitions taken from A to B includes the transition that has cast() function. What would the SMC query be like to do this?

Estimate the probability of reaching B within 100 time units:

Pr[<=100](<> Process.B)

If you need specifically from A, then you need to add a variable seenA which is set to true whenever A is visited, then the query:

Pr[<=100](<> seenA && Process.B)

Best regards,
Marius