You can not select more than 25 topics Topics must start with a letter or number, can include dashes ('-') and can be up to 35 characters long.
 
 
 
 
 
 

253 lines
9.1 KiB

HTTP/1.1 200 OK Content-Type: text/html; charset=UTF-8 Set-Cookie: i_like_gitea=5a858861d894ee7f; Path=/; HttpOnly; SameSite=Lax Set-Cookie: _csrf=MX1ySu7voI16-zWHTP7ymjCwEnw6MTczNTAwNDc2NDQyMjY0ODMyNg; Path=/; Expires=Wed, 25 Dec 2024 01:46:04 GMT; HttpOnly; SameSite=Lax Set-Cookie: macaron_flash=; Path=/; Max-Age=0; HttpOnly; SameSite=Lax X-Frame-Options: SAMEORIGIN Date: Tue, 24 Dec 2024 01:46:04 GMT Transfer-Encoding: chunked 37a27 sp/cln_mirror - doc/polynomial/diag_rational.lyx at c76df3d0b21dca2c26eadf60edacd7ce195aca21 - cln_mirror - Gitea: Git with a cup of tea
You can not select more than 25 topics Topics must start with a letter or number, can include dashes ('-') and can be up to 35 characters long.
 
 
 
 
 

763 lines
13 KiB

import os
import stormpy
from configurations import gspn, xml
@gspn
class TestGSPNBuilder:
def test_layout_info(self):
layout = stormpy.gspn.LayoutInfo()
assert layout.x == 0
assert layout.y == 0
assert layout.rotation == 0
layout.x = 1
assert layout.x == 1
layout_xy = stormpy.gspn.LayoutInfo(2, 3)
assert layout_xy.x == 2
assert layout_xy.rotation == 0
layout_xyr = stormpy.gspn.LayoutInfo(2, 3, 4)
assert layout_xyr.rotation == 4
def test_place(self):
p_id = 4
place = stormpy.gspn.Place(id=p_id)
assert p_id == place.get_id()
assert not place.has_restricted_capacity()
place.set_capacity(cap=5)
assert place.has_restricted_capacity()
assert place.get_capacity() == 5
p_name = "P_0"
place.set_name(name=p_name)
assert place.get_name() == p_name
p_tokens = 2
place.set_number_of_initial_tokens(p_tokens)
assert place.get_number_of_initial_tokens() == p_tokens
def test_transition(self):
# test TimedTransition
tt = stormpy.gspn.TimedTransition()
tt_name = " tt"
tt.set_name(tt_name)
assert tt_name == tt.get_name()
tt_rate = 0.2
tt.set_rate(tt_rate)
assert tt_rate == tt.get_rate()
# connect a place to this transition and test arcs
place = stormpy.gspn.Place(0)
# test input arcs
assert not tt.exists_input_arc(place)
tt.set_input_arc_multiplicity(place, 2)
assert tt.exists_input_arc(place)
assert tt.get_input_arc_multiplicity(place) == 2
tt.remove_input_arc(place)
assert not tt.exists_input_arc(place)
# test output arcs
assert not tt.exists_output_arc(place)
tt.set_output_arc_multiplicity(place, 3)
assert tt.exists_output_arc(place)
assert tt.get_output_arc_multiplicity(place) == 3
tt.remove_output_arc(place)
assert not tt.exists_output_arc(place)
# test inhibition arcs
assert not tt.exists_inhibition_arc(place)
tt.set_inhibition_arc_multiplicity(place, 5)
assert tt.exists_inhibition_arc(place)
assert tt.get_inhibition_arc_multiplicity(place) == 5
tt.remove_inhibition_arc(place)
assert not tt.exists_inhibition_arc(place)
# test ImmediateTransition
ti = stormpy.gspn.ImmediateTransition()
ti_name = " ti"
ti.set_name(ti_name)
assert ti_name == ti.get_name()
assert ti.no_weight_attached()
ti_weight = 0.2
ti.set_weight(ti_weight)
assert ti_weight == ti.get_weight()
assert not ti.no_weight_attached()
def test_build_gspn(self):
gspn_name = "gspn_test"
builder = stormpy.gspn.GSPNBuilder()
id_p_0 = builder.add_place()
id_p_1 = builder.add_place(initial_tokens=1)
id_p_2 = builder.add_place(initial_tokens=0, name="place_2")
id_p_3 = builder.add_place(capacity=2, initial_tokens=3, name="place_3")
p_layout = stormpy.gspn.LayoutInfo(1, 2)
builder.set_place_layout_info(id_p_0, p_layout)
id_ti_0 = builder.add_immediate_transition(priority=1, weight=0.5, name="ti_0")
id_ti_1 = builder.add_immediate_transition()
id_tt_0 = builder.add_timed_transition(priority=2, rate=0.4, name="tt_0")
id_tt_1 = builder.add_timed_transition(priority=0, rate=0.5, num_servers=2, name="tt_1")
t_layout = stormpy.gspn.LayoutInfo(1, 2)
builder.set_transition_layout_info(id_ti_0, t_layout)
# add arcs
builder.add_input_arc(id_p_0, id_ti_1, multiplicity=2)
builder.add_input_arc("place_2", "ti_0", multiplicity=2)
builder.add_output_arc(id_ti_1, id_p_2, multiplicity=2)
builder.add_output_arc("tt_0", "place_3", multiplicity=2)
builder.add_inhibition_arc(id_p_2, id_tt_0, multiplicity=2)
builder.add_inhibition_arc("place_3", "tt_0", multiplicity=2)
builder.add_normal_arc("place_3", "tt_0", multiplicity=2)
builder.add_normal_arc("tt_0", "place_3", multiplicity=2)
# test gspn composition
builder.set_name(gspn_name)
gspn = builder.build_gspn()
assert gspn.get_name() == gspn_name
assert gspn.is_valid()
assert gspn.get_number_of_immediate_transitions() == 2
assert gspn.get_number_of_timed_transitions() == 2
assert gspn.get_number_of_places() == 4
assert len(gspn.get_places()) == 4
assert len(gspn.get_immediate_transitions()) == 2
assert len(gspn.get_timed_transitions()) == 2
# test places
p_0 = gspn.get_place(id_p_0)
assert p_0.get_id() == id_p_0
p_1 = gspn.get_place(id_p_1)
assert p_1.get_id() == id_p_1
assert p_1.get_number_of_initial_tokens() == 1
p_2 = gspn.get_place(id_p_2)
assert p_2.get_id() == id_p_2
assert p_2.get_name() == "place_2"
p_3 = gspn.get_place(id_p_3)
assert p_3.get_name() == "place_3"
assert p_3.get_capacity() == 2
assert p_3.get_number_of_initial_tokens() == 3
assert p_3.has_restricted_capacity()
# test transitions
ti_0 = gspn.get_immediate_transition("ti_0")
assert ti_0.get_id() == id_ti_0
assert ti_0.get_weight() == 0.5
assert ti_0.get_priority() == 1
tt_0 = gspn.get_timed_transition("tt_0")
assert tt_0.get_id() == id_tt_0
assert tt_0.get_rate() == 0.4
assert tt_0.get_priority() == 2
tt_1 = gspn.get_timed_transition("tt_1")
assert tt_1.get_id() == id_tt_1
assert tt_1.get_number_of_servers() == 2
# test new name
gspn_new_name = "new_name"
gspn.set_name(gspn_new_name)
assert gspn.get_name() == gspn_new_name
def test_export_to_pnpro(self, tmpdir):
builder = stormpy.gspn.GSPNBuilder()
builder.set_name("gspn_test")
# add places and transitions
id_p_0 = builder.add_place()
id_p_1 = builder.add_place(initial_tokens=3, name="place_1", capacity=2)
id_ti_0 = builder.add_immediate_transition(priority=0, weight=0.5, name="ti_0")
id_tt_0 = builder.add_timed_transition(priority=0, rate=0.5, num_servers=2, name="tt_0")
gspn = builder.build_gspn()
export_file = os.path.join(str(tmpdir), "gspn.pnpro")
# export gspn to pnml
gspn.export_gspn_pnpro_file(export_file)
# import gspn
gspn_parser = stormpy.gspn.GSPNParser()
gspn_import = gspn_parser.parse(export_file)
# test imported gspn
assert gspn_import.get_name() == gspn.get_name()
assert gspn_import.get_number_of_timed_transitions() == gspn.get_number_of_timed_transitions()
assert gspn_import.get_number_of_immediate_transitions() == gspn.get_number_of_immediate_transitions()
assert gspn_import.get_number_of_places() == gspn.get_number_of_places()
p_0 = gspn_import.get_place(id_p_0)
assert p_0.get_id() == id_p_0
p_1 = gspn_import.get_place(id_p_1)
assert p_1.get_name() == "place_1"
# todo capacity info lost
# assert p_1.get_capacity() == 2
# assert p_1.has_restricted_capacity() == True
assert p_1.get_number_of_initial_tokens() == 3
ti_0 = gspn_import.get_immediate_transition("ti_0")
assert ti_0.get_id() == id_ti_0
tt_0 = gspn_import.get_timed_transition("tt_0")
assert tt_0.get_id() == id_tt_0
@xml
def test_export_to_pnml(self, tmpdir):
builder = stormpy.gspn.GSPNBuilder()
builder.set_name("gspn_test")
# add places and transitions
id_p_0 = builder.add_place()
id_p_1 = builder.add_place(initial_tokens=3, name="place_1", capacity=2)
id_ti_0 = builder.add_immediate_transition(priority=0, weight=0.5, name="ti_0")
id_tt_0 = builder.add_timed_transition(priority=0, rate=0.5, num_servers=2, name="tt_0")
gspn = builder.build_gspn()
export_file = os.path.join(str(tmpdir), "gspn.pnml")
# export gspn to pnml
gspn.export_gspn_pnml_file(export_file)
# import gspn
gspn_parser = stormpy.gspn.GSPNParser()
gspn_import = gspn_parser.parse(export_file)
# test imported gspn
assert gspn_import.get_name() == gspn.get_name()
assert gspn_import.get_number_of_timed_transitions() == gspn.get_number_of_timed_transitions()
assert gspn_import.get_number_of_immediate_transitions() == gspn.get_number_of_immediate_transitions()
assert gspn_import.get_number_of_places() == gspn.get_number_of_places()
p_0 = gspn_import.get_place(id_p_0)
assert p_0.get_id() == id_p_0
p_1 = gspn_import.get_place(id_p_1)
assert p_1.get_name() == "place_1"
assert p_1.get_capacity() == 2
assert p_1.get_number_of_initial_tokens() == 3
assert p_1.has_restricted_capacity()
ti_0 = gspn_import.get_immediate_transition("ti_0")
assert ti_0.get_id() == id_ti_0
tt_0 = gspn_import.get_timed_transition("tt_0")
#This file was created by <bruno> Sun Feb 16 14:19:06 1997
#LyX 0.10 (C) 1995 1996 Matthias Ettrich and the LyX Team
\lyxformat 2.10
\textclass article
\begin_preamble
\catcode`@=11 % @ ist ab jetzt ein gewoehnlicher Buchstabe
\def\Res{\mathop{\operator@font Res}}
\def\ll{\langle\!\langle}
\def\gg{\rangle\!\rangle}
\catcode`@=12 % @ ist ab jetzt wieder ein Sonderzeichen
\end_preamble
\language default
\inputencoding latin1
\fontscheme default
\epsfig dvips
\papersize a4paper
\paperfontsize 12
\baselinestretch 1.00
\secnumdepth 3
\tocdepth 3
\paragraph_separation indent
\quotes_language english
\quotes_times 2
\paperorientation portrait
\papercolumns 0
\papersides 1
\paperpagestyle plain
\layout LaTeX Title
The diagonal of a rational function
\layout Description
Theorem:
\layout Standard
Let
\begin_inset Formula \( M \)
\end_inset
be a torsion-free
\begin_inset Formula \( R \)
\end_inset
-module, and
\begin_inset Formula \( d>0 \)
\end_inset
.
Let
\begin_inset Formula
\[
f=\sum _{n_{1},...,n_{d}}a_{n_{1},...,n_{d}}\, x_{1}^{n_{1}}\cdots x_{d}^{n_{d}}\in M[[x_{1},\ldots x_{d}]]\]
\end_inset
be a rational function, i.
e.
there are
\begin_inset Formula \( P\in M[x_{1},\ldots ,x_{d}] \)
\end_inset
and
\begin_inset Formula \( Q\in R[x_{1},\ldots ,x_{d}] \)
\end_inset
with
\begin_inset Formula \( Q(0,\ldots ,0)=1 \)
\end_inset
and
\begin_inset Formula \( Q\cdot f=P \)
\end_inset
.
Then the full diagonal of
\begin_inset Formula \( f \)
\end_inset
\begin_inset Formula
\[
g=\sum ^{\infty }_{n=0}a_{n,\ldots ,n}\, x_{1}^{n}\]
\end_inset
is a D-finite element of
\begin_inset Formula \( M[[x_{1}]] \)
\end_inset
, w.
r.
t.
\begin_inset Formula \( R[x_{1}] \)
\end_inset
and
\begin_inset Formula \( \{\partial _{x_{1}}\} \)
\end_inset
.
\layout Description
Proof:
\layout Standard
From the hypotheses,
\begin_inset Formula \( M[[x_{1},\ldots ,x_{d}]] \)
\end_inset
is a torsion-free differential module over
\begin_inset Formula \( R[x_{1},\ldots ,x_{d}] \)
\end_inset
w.
r.
t.
the derivatives
\begin_inset Formula \( \{\partial _{x_{1}},\ldots ,\partial _{x_{d}}\} \)
\end_inset
, and
\begin_inset Formula \( f \)
\end_inset
is a D-finite element of
\begin_inset Formula \( M[[x_{1},\ldots ,x_{d}]] \)
\end_inset
over
\begin_inset Formula \( R[x_{1},\ldots ,x_{d}] \)
\end_inset
w.
r.
t.
\begin_inset Formula \( \{\partial _{x_{1}},\ldots ,\partial _{x_{d}}\} \)
\end_inset
.
Now apply the general diagonal theorem ([1], section 2.
18)
\begin_inset Formula \( d-1 \)
\end_inset
times.
\layout Description
Theorem:
\layout Standard
Let
\begin_inset Formula \( R \)
\end_inset
be an integral domain of characteristic 0 and
\begin_inset Formula \( M \)
\end_inset
simultaneously a torsion-free
\begin_inset Formula \( R \)
\end_inset
-module and a commutative
\begin_inset Formula \( R \)
\end_inset
-algebra without zero divisors.
Let
\begin_inset Formula
\[
f=\sum _{m,n\geq 0}a_{m,n}x^{m}y^{n}\in M[[x,y]]\]
\end_inset
be a rational function.
Then the diagonal of
\begin_inset Formula \( f \)
\end_inset
\begin_inset Formula
\[
g=\sum ^{\infty }_{n=0}a_{n,n}\, x^{n}\]
\end_inset
is algebraic over
\begin_inset Formula \( R[x] \)
\end_inset
.
\layout Description
Motivation
\protected_separator
of
\protected_separator
proof:
\layout Standard
The usual proof ([2]) uses complex analysis and works only for
\begin_inset Formula \( R=M=C \)
\end_inset
.
The idea is to compute
\begin_inset Formula
\[
g(x^{2})=\frac{1}{2\pi i}\oint _{|z|=1}f(xz,\frac{x}{z})\frac{dz}{z}\]
\end_inset
This integral, whose integrand is a rational function in
\begin_inset Formula \( x \)
\end_inset
and
\begin_inset Formula \( z \)
\end_inset
, is calculated using the residue theorem.
Since
\begin_inset Formula \( f(x,y) \)
\end_inset
is continuous at
\begin_inset Formula \( (0,0) \)
\end_inset
, there is a
\begin_inset Formula \( \delta >0 \)
\end_inset
such that
\begin_inset Formula \( f(x,y)\neq \infty \)
\end_inset
for
\begin_inset Formula \( |x|<\delta \)
\end_inset
</