6 Представления неподвижной точки в CTL. Алгоритм символьной верификации моделей в CTL (1185958)
Текст из файла
Âåðèôèêàöèÿìîäåëåé ïðîãðàììËÅÊÒÎÐ:Âëàäèìèð Àíàòîëüåâè÷ Çàõàðîâzakh@cs.msu.suËåêöèÿ 6.Ñèìâîëüíûé àëãîðèòìâåðèôèêàöèè ìîäåëåé äëÿ CTL1.Ïðåäïîñûëêè äëÿ ñèìâîëüíûõàëãîðèòìîâ âåðèôèêàöèè2.Ïðåäñòàâëåíèÿ íåïîäâèæíîéòî÷êè3.Íåïîäâèæíûå òî÷êè èòåìïîðàëüíûå îïåðàòîðû4.Ñèìâîëüíàÿ âåðèôèêàöèÿìîäåëåé äëÿ CTLÏðåäïîñûëêè äëÿ ñèìâîëüíîé âåðèôèêàöèè1. Áóëåâû ôóíêöèè ïðåäñòàâèìû ROBDD;Ïðåäïîñûëêè äëÿ ñèìâîëüíîé âåðèôèêàöèè1. Áóëåâû ôóíêöèè ïðåäñòàâèìû ROBDD;2. Äëÿ ROBDD èìåþòñÿ ýôôåêòèâíûå ïðîöåäóðûf (x̄) = g (x̄) ,f (x̄){xi /c} ,îïåðàöèé f (x̄) ∗ g (x̄) ;I ïðîâåðêè ðàâåíñòâà áóëåâûõ ôóíêöèéI ïîäñòàíîâêè êîíñòàíòI âû÷èñëåíèÿ áóëåâûõÏðåäïîñûëêè äëÿ ñèìâîëüíîé âåðèôèêàöèè1. Áóëåâû ôóíêöèè ïðåäñòàâèìû ROBDD;2.
Äëÿ ROBDD èìåþòñÿ ýôôåêòèâíûå ïðîöåäóðûf (x̄) = g (x̄) ,f (x̄){xi /c} ,îïåðàöèé f (x̄) ∗ g (x̄) ;I ïðîâåðêè ðàâåíñòâà áóëåâûõ ôóíêöèéI ïîäñòàíîâêè êîíñòàíòI âû÷èñëåíèÿ áóëåâûõ3. Ìíîæåñòâî ñîñòîÿíèé S ìîäåëè Êðèïêå M = (S, S0, R, L)êîäèðóåòñÿ äâîè÷íûìè íàáîðàìè (σ1, σ2, . .
. , σn ) ;Ïðåäïîñûëêè äëÿ ñèìâîëüíîé âåðèôèêàöèè1. Áóëåâû ôóíêöèè ïðåäñòàâèìû ROBDD;2. Äëÿ ROBDD èìåþòñÿ ýôôåêòèâíûå ïðîöåäóðûf (x̄) = g (x̄) ,f (x̄){xi /c} ,îïåðàöèé f (x̄) ∗ g (x̄) ;I ïðîâåðêè ðàâåíñòâà áóëåâûõ ôóíêöèéI ïîäñòàíîâêè êîíñòàíòI âû÷èñëåíèÿ áóëåâûõ3. Ìíîæåñòâî ñîñòîÿíèé S ìîäåëè Êðèïêå M = (S, S0, R, L)êîäèðóåòñÿ äâîè÷íûìè íàáîðàìè (σ1, σ2, . . .
, σn ) ;4. Îòíîøåíèå ïåðåõîäîâ R ìîäåëè Êðèïêå M = (S, S0, R, L)ðàññìàòðèâàåòñÿ êàê áóëåâà ôóíêöèÿ R(x̄, x̄ 0) , êîòîðàÿçàâèñèò îò ïåðåìåííûõ, ïðåäñòàâëÿþùèõ ñîñòîÿíèÿìîäåëè;Ïðåäïîñûëêè äëÿ ñèìâîëüíîé âåðèôèêàöèè1. Áóëåâû ôóíêöèè ïðåäñòàâèìû ROBDD;2. Äëÿ ROBDD èìåþòñÿ ýôôåêòèâíûå ïðîöåäóðûf (x̄) = g (x̄) ,f (x̄){xi /c} ,îïåðàöèé f (x̄) ∗ g (x̄) ;I ïðîâåðêè ðàâåíñòâà áóëåâûõ ôóíêöèéI ïîäñòàíîâêè êîíñòàíòI âû÷èñëåíèÿ áóëåâûõ3. Ìíîæåñòâî ñîñòîÿíèé S ìîäåëè Êðèïêå M = (S, S0, R, L)êîäèðóåòñÿ äâîè÷íûìè íàáîðàìè (σ1, σ2, .
. . , σn ) ;4. Îòíîøåíèå ïåðåõîäîâ R ìîäåëè Êðèïêå M = (S, S0, R, L)ðàññìàòðèâàåòñÿ êàê áóëåâà ôóíêöèÿ R(x̄, x̄ 0) , êîòîðàÿçàâèñèò îò ïåðåìåííûõ, ïðåäñòàâëÿþùèõ ñîñòîÿíèÿìîäåëè;5. Ôóíêöèÿ ðàçìåòêè L ìîäåëè Êðèïêå M = (S, S0, R, L)ðàññìàòðèâàåòñÿ êàê íàáîð áóëåâûõ ôóíêöèéLp (x̄), p ∈ AP , âûäåëÿþùèõ òå ñîñòîÿíèÿ, íà êîòîðûõâûïîëíèìû àòîìàðíûå ôîðìóëû.Ïðåäïîñûëêè äëÿ ñèìâîëüíîé âåðèôèêàöèèÎïåðàöèè íàä ìíîæåñòâàìè è îòíîøåíèÿìè ìîäåëèðóþòñÿîïåðàöèÿìè íàä áóëåâûìè ôóíêöèÿìè:I ïåðåñå÷åíèå: A ∩ B = C =⇒ fC = fA ∧ fB ,I îáúåäèíåíèå: A ∪ B = C =⇒ fC = fA ∨ fB ,I äîïîëíåíèå: S \ A = C =⇒ fC = ¬fA ,I îáðàç: R(A) = C =⇒ fC = ∃x̄(fA (x̄) ∧ R(x̄, ȳ )) ,I ïðîîáðàç: R −1 (A) = C =⇒ fC = ∃ȳ (fA (ȳ ) ∧ R(x̄, ȳ )) .Çäåñü ∃y h(x, y ) = h(x, 0) ∨ h(x, 1) .Ïðåäïîñûëêè äëÿ ñèìâîëüíîé âåðèôèêàöèèÀëãîðèòìû àíàëèçà ìîäåëåé, èñïîëüçóþùèå èõ ïðåäñòàâëåíèÿâ âèäå OBDD, íàçûâàþòñÿ ñèìâîëüíûì èëè íåÿâíûìè ,ïîñêîëüêó îí îïåðèðóåò íå ñ ñàìèìè ìíîæåñòâàìè, ýëåìåíòûêîòîðûõ ÿâíî ïåðå÷èñëåíû, à ñ ñèìâîëüíûìè îïèñàíèÿìè(ïðåäñòàâëåíèÿìè) ìíîæåñòâ.Êîãäà ìîäåëü èìååò áîëüøîé ðàçìåð (≥ 232 ), ïðèõîäèòñÿîïåðèðîâàòü ñ öåëûìè ìíîæåñòâàìè, à íå ñ îòäåëüíûìèñîñòîÿíèÿìè è ïåðåõîäàìè.
Òàáëè÷íûå àëãîðèòìû modelchecking äëÿ ýòîé öåëè íåïðèãîäíû. Íóæíû èòåðàòèâíûåàëãîðèòìû, ðàáîòàþùèå ñ îïèñàíèÿìè ìíîæåñòâ.Äëÿ ýòîãî âîñïîëüçóåìñÿ îïðåäåëåíèåì îïåðàòîðîâòåìïîðàëüíîé ëîãèêè â òåðìèíàõ íåïîäâèæíîé òî÷êè .Ïîêàæåì, êàê îïèñàòü ìíîæåñòâî ñîñòîÿíèé, óäîâëåòâîðÿþùèõíåêîòîðîé CTL-ôîðìóëå, ïðè ïîìîùè íàèìåíüøåé èëèíàèáîëüøåé íåïîäâèæíîé òî÷êè ïîäõîäÿùåé ôóíêöèè.Ïðåäñòàâëåíèÿ íåïîäâèæíîé òî÷êèÏóñòü çàäàíà ïðîèçâîëüíàÿ ìîäåëü Êðèïêå M = (S, S0, R, L) ñêîíå÷íûì ìíîæåñòâîì ñîñòîÿíèé.Ñîâîêóïíîñòü ℘(S) âñåõ ïîäìíîæåñòâ ìíîæåñòâà S îáðàçóåòðåøåòêó ïî îòíîøåíèþ âêëþ÷åíèÿ ⊆ :I òî÷íàÿ âåðõíÿÿ ãðàíü sup(S1 , S2 ) = S1 ∪ S2 ,I òî÷íàÿ íèæíÿÿ ãðàíü inf (S1 , S2 ) = S1 ∩ S2 ,Âñÿêèé ýëåìåíò S 0 ðåøåòêè (℘(S), ⊆) ìîæåò ðàññìàòðèâàòüñÿêàê ïðåäèêàò (îòíîøåíèå) íà S , ïðèíèìàþùèé çíà÷åíèå true âòî÷íîñòè íà âñåõ ñîñòîÿíèÿõ èç S 0 .Íàèìåíüøèì ýëåìåíòîì ðåøåòêè ÿâëÿåòñÿ ïóñòîå ìíîæåñòâî,êîòîðîå áóäåò îáîçíà÷àòüñÿ False , à íàèáîëüøèì ýëåìåíòîìðåøåòêè ñëóæèò ñàìî ìíîæåñòâî S , êîòîðîå ìû áóäåìîáîçíà÷àòü True .Ôóíêöèþ, îòîáðàæàþùóþ ℘(S) â ℘(S) , áóäåì íàçûâàòüïðåîáðàçîâàòåëåì ïðåäèêàòîâ .Ïðåäñòàâëåíèÿ íåïîäâèæíîé òî÷êèÏóñòü τ : ℘(S) → ℘(S) îäèí èç òàêèõ ïðåîáðàçîâàòåëåéïðåäèêàòîâ.
Òîãäà1) Ôóíêöèÿ τ ñ÷èòàåòñÿ ìîíîòîííîé , åñëè èç âêëþ÷åíèÿP ⊆ Q ñëåäóåò τ (P) ⊆ τ (Q) ;2) Ôóíêöèÿ τ ñ÷èòàåòñÿ ∪-íåïðåðûâíîé , åñëè äëÿ âñÿêîéìîíîòîííî íåóáûâàþùåé ïîñëåäîâàòåëüíîñòèïðåäèêàòîâ∞∞SSτ (Pi ) ;P1 ⊆ P2 ⊆ . . . âåðíî ðàâåíñòâî τ ( Pi ) =i=1i=13) Ôóíêöèÿ τ ñ÷èòàåòñÿ ∩-íåïðåðûâíîé , åñëè äëÿ âñÿêîéìîíîòîííî íåâîçðàñòàþùåé ïîñëåäîâàòåëüíîñòè∞∞ïðåäèêàòîâ P1 ⊇ P2 ⊇ .
. . âåðíî τ ( T Pi ) = T τ (Pi )i=1i=1Ïðåäèêàò P íàçûâàåòñÿ íåïîäâèæíîé òî÷êîé ïðåîáðàçîâàòåëÿτ , åñëè èìååò ìåñòî ðàâåíñòâî τ (P) = P .Ïðåäñòàâëåíèÿ íåïîäâèæíîé òî÷êèÓ ìîíîòîííîãî ïðåîáðàçîâàòåëÿ τ íà ℘(S) âñåãäà åñòüíàèìåíüøàÿ íåïîäâèæíàÿ òî÷êà µZ . τ (Z ) èíàèáîëüøàÿ íåïîäâèæíàÿ òî÷êà νZ . τ (Z )Íàèìåíüøàÿ íåïîäâèæíàÿ òî÷êà èìååò âèäµZ . τ (Z ) = ∩{Z | τ (Z ) ⊆ Z }äëÿ ìîíîòîííîãîτ , è ïðè ýòîì∞Sτ i (False),µZ .
τ (Z ) =i=1åñëè ïðåîáðàçîâàòåëü τ ÿâëÿåòñÿ ∪ -íåïðåðûâíûì.Àíàëîãè÷íî, íàèáîëüøàÿ íåïîäâèæíàÿ òî÷êà èìååò âèäνZ . τ (Z ) = ∪{Z | τ (Z ) ⊇ Z }τ∞TµZ . τ (Z ) =τ i (True)äëÿ ìîíîòîííîãî , è ïðè ýòîì,i=1åñëè ïðåîáðàçîâàòåëü τ ÿâëÿåòñÿ ∩ -íåïðåðûâíûì.Ïðåäñòàâëåíèÿ íåïîäâèæíîé òî÷êèÓ ìîíîòîííîãî ïðåîáðàçîâàòåëÿ τ íà ℘(S) âñåãäà åñòüíàèìåíüøàÿ íåïîäâèæíàÿ òî÷êà µZ . τ (Z ) èíàèáîëüøàÿ íåïîäâèæíàÿ òî÷êà νZ . τ (Z )Íàèìåíüøàÿ íåïîäâèæíàÿ òî÷êà èìååò âèäµZ . τ (Z ) = ∩{Z | τ (Z ) ⊆ Z }äëÿ ìîíîòîííîãîτ , è ïðè ýòîì∞Sτ i (False),µZ .
τ (Z ) =i=1åñëè ïðåîáðàçîâàòåëü τ ÿâëÿåòñÿ ∪ -íåïðåðûâíûì.Àíàëîãè÷íî, íàèáîëüøàÿ íåïîäâèæíàÿ òî÷êà èìååò âèäνZ . τ (Z ) = ∪{Z | τ (Z ) ⊇ Z }τ∞TµZ . τ (Z ) =τ i (True)äëÿ ìîíîòîííîãî , è ïðè ýòîì,i=1åñëè ïðåîáðàçîâàòåëü τ ÿâëÿåòñÿ ∩ -íåïðåðûâíûì.Ïîïðîáóéòå äîêàçàòü ñàìîñòîÿòåëüíî. Ýòî íåñëîæíûéìàòåìàòè÷åñêèé ýòþä èç òåîðèè ìíîæåñòâ.Ïðåäñòàâëåíèÿ íåïîäâèæíîé òî÷êèÑëåäóþùèå ëåììû âåñüìà ïîëåçíû, êîãäà ïðèõîäèòñÿ èìåòüäåëî ñ ïðåîáðàçîâàòåëÿìè ïðåäèêàòîâ, îïðåäåëåííûìè íàêîíå÷íûõ ìîäåëÿõ Êðèïêå.Ëåììà 1. Åñëè S êîíå÷íîå ìíîæåñòâî, à τ ìîíîòîííûéïðåîáðàçîâàòåëü, òî τ òàêæå ∪ -íåïðåðûâåí è ∩ -íåïðåðûâåí.Äîê-âî: Ðàññìîòðèì ïîñëåäîâàòåëüíîñòü P1 ⊆ P2 ⊆ . .
.ïîäìíîæåñòâ ìíîæåñòâà S .Ïðåäñòàâëåíèÿ íåïîäâèæíîé òî÷êèÑëåäóþùèå ëåììû âåñüìà ïîëåçíû, êîãäà ïðèõîäèòñÿ èìåòüäåëî ñ ïðåîáðàçîâàòåëÿìè ïðåäèêàòîâ, îïðåäåëåííûìè íàêîíå÷íûõ ìîäåëÿõ Êðèïêå.Ëåììà 1. Åñëè S êîíå÷íîå ìíîæåñòâî, à τ ìîíîòîííûéïðåîáðàçîâàòåëü, òî τ òàêæå ∪ -íåïðåðûâåí è ∩ -íåïðåðûâåí.Äîê-âî: Ðàññìîòðèì ïîñëåäîâàòåëüíîñòü P1 ⊆ P2 ⊆ . . .ïîäìíîæåñòâ ìíîæåñòâà S . Òàê êàê S êîíå÷íîå ìíîæåñòâî,ñóùåñòâóåò òàêîå j0 , ÷òî Pj = Pj äëÿ ëþáîãî j > j0 .
Ïðè ýòîìPj ⊆ Pj äëÿ êàæäîãî j < j0 .00Ïðåäñòàâëåíèÿ íåïîäâèæíîé òî÷êèÑëåäóþùèå ëåììû âåñüìà ïîëåçíû, êîãäà ïðèõîäèòñÿ èìåòüäåëî ñ ïðåîáðàçîâàòåëÿìè ïðåäèêàòîâ, îïðåäåëåííûìè íàêîíå÷íûõ ìîäåëÿõ Êðèïêå.Ëåììà 1. Åñëè S êîíå÷íîå ìíîæåñòâî, à τ ìîíîòîííûéïðåîáðàçîâàòåëü, òî τ òàêæå ∪ -íåïðåðûâåí è ∩ -íåïðåðûâåí.Äîê-âî: Ðàññìîòðèì ïîñëåäîâàòåëüíîñòü P1 ⊆ P2 ⊆ .
. .ïîäìíîæåñòâ ìíîæåñòâà S . Òàê êàê S êîíå÷íîå ìíîæåñòâî,ñóùåñòâóåò òàêîå j0 , ÷òî Pj = Pj äëÿ ëþáîãî j > j0 . Ïðè ýòîìPj ⊆ Pj äëÿ êàæäîãî j < j0 . Òàêèì îáðàçîì, ∪i Pi = Pj , èâñëåäñòâèå ýòîãî ìû ïîëó÷àåì τ (∪i Pi ) = τ (Pj ) .0000Ïðåäñòàâëåíèÿ íåïîäâèæíîé òî÷êèÑëåäóþùèå ëåììû âåñüìà ïîëåçíû, êîãäà ïðèõîäèòñÿ èìåòüäåëî ñ ïðåîáðàçîâàòåëÿìè ïðåäèêàòîâ, îïðåäåëåííûìè íàêîíå÷íûõ ìîäåëÿõ Êðèïêå.Ëåììà 1. Åñëè S êîíå÷íîå ìíîæåñòâî, à τ ìîíîòîííûéïðåîáðàçîâàòåëü, òî τ òàêæå ∪ -íåïðåðûâåí è ∩ -íåïðåðûâåí.Äîê-âî: Ðàññìîòðèì ïîñëåäîâàòåëüíîñòü P1 ⊆ P2 ⊆ . .
.ïîäìíîæåñòâ ìíîæåñòâà S . Òàê êàê S êîíå÷íîå ìíîæåñòâî,ñóùåñòâóåò òàêîå j0 , ÷òî Pj = Pj äëÿ ëþáîãî j > j0 . Ïðè ýòîìPj ⊆ Pj äëÿ êàæäîãî j < j0 . Òàêèì îáðàçîì, ∪i Pi = Pj , èâñëåäñòâèå ýòîãî ìû ïîëó÷àåì τ (∪i Pi ) = τ (Pj ) . Ñ äðóãîéñòîðîíû, â ñèëó ìîíîòîííîñòè τ ìû èìååì0000τ (P1 ) ⊆ τ (P2 ) ⊆ . . .Ïðåäñòàâëåíèÿ íåïîäâèæíîé òî÷êèÑëåäóþùèå ëåììû âåñüìà ïîëåçíû, êîãäà ïðèõîäèòñÿ èìåòüäåëî ñ ïðåîáðàçîâàòåëÿìè ïðåäèêàòîâ, îïðåäåëåííûìè íàêîíå÷íûõ ìîäåëÿõ Êðèïêå.Ëåììà 1. Åñëè S êîíå÷íîå ìíîæåñòâî, à τ ìîíîòîííûéïðåîáðàçîâàòåëü, òî τ òàêæå ∪ -íåïðåðûâåí è ∩ -íåïðåðûâåí.Äîê-âî: Ðàññìîòðèì ïîñëåäîâàòåëüíîñòü P1 ⊆ P2 ⊆ . . .ïîäìíîæåñòâ ìíîæåñòâà S . Òàê êàê S êîíå÷íîå ìíîæåñòâî,ñóùåñòâóåò òàêîå j0 , ÷òî Pj = Pj äëÿ ëþáîãî j > j0 .
Ïðè ýòîìPj ⊆ Pj äëÿ êàæäîãî j < j0 . Òàêèì îáðàçîì, ∪i Pi = Pj , èâñëåäñòâèå ýòîãî ìû ïîëó÷àåì τ (∪i Pi ) = τ (Pj ) . Ñ äðóãîéñòîðîíû, â ñèëó ìîíîòîííîñòè τ ìû èìååìτ (P1 ) ⊆ τ (P2 ) ⊆ . . . Ïîýòîìó τ (Pj ) ⊆ τ (Pj ) äëÿ êàæäîãîj < j0 , è τ (Pj ) = τ (Pj ) äëÿ êàæäîãî j > j0 .000000Ïðåäñòàâëåíèÿ íåïîäâèæíîé òî÷êèÑëåäóþùèå ëåììû âåñüìà ïîëåçíû, êîãäà ïðèõîäèòñÿ èìåòüäåëî ñ ïðåîáðàçîâàòåëÿìè ïðåäèêàòîâ, îïðåäåëåííûìè íàêîíå÷íûõ ìîäåëÿõ Êðèïêå.Ëåììà 1.
Åñëè S êîíå÷íîå ìíîæåñòâî, à τ ìîíîòîííûéïðåîáðàçîâàòåëü, òî τ òàêæå ∪ -íåïðåðûâåí è ∩ -íåïðåðûâåí.Äîê-âî: Ðàññìîòðèì ïîñëåäîâàòåëüíîñòü P1 ⊆ P2 ⊆ . . .ïîäìíîæåñòâ ìíîæåñòâà S . Òàê êàê S êîíå÷íîå ìíîæåñòâî,ñóùåñòâóåò òàêîå j0 , ÷òî Pj = Pj äëÿ ëþáîãî j > j0 . Ïðè ýòîìPj ⊆ Pj äëÿ êàæäîãî j < j0 . Òàêèì îáðàçîì, ∪i Pi = Pj , èâñëåäñòâèå ýòîãî ìû ïîëó÷àåì τ (∪i Pi ) = τ (Pj ) .
Ñ äðóãîéñòîðîíû, â ñèëó ìîíîòîííîñòè τ ìû èìååìτ (P1 ) ⊆ τ (P2 ) ⊆ . . . Ïîýòîìó τ (Pj ) ⊆ τ (Pj ) äëÿ êàæäîãîj < j0 , è τ (Pj ) = τ (Pj ) äëÿ êàæäîãî j > j0 .  ðåçóëüòàòåïîëó÷àåì ñîîòíîøåíèå ∪i τ (Pi ) = τ (Pj ) , à ýòî îçíà÷àåò, ÷òîïðåîáðàçîâàòåëü τ ÿâëÿåòñÿ ∪ -íåïðåðûâíûì.0000000Ïðåäñòàâëåíèÿ íåïîäâèæíîé òî÷êèÑëåäóþùèå ëåììû âåñüìà ïîëåçíû, êîãäà ïðèõîäèòñÿ èìåòüäåëî ñ ïðåîáðàçîâàòåëÿìè ïðåäèêàòîâ, îïðåäåëåííûìè íàêîíå÷íûõ ìîäåëÿõ Êðèïêå.Ëåììà 1.
Åñëè S êîíå÷íîå ìíîæåñòâî, à τ ìîíîòîííûéïðåîáðàçîâàòåëü, òî τ òàêæå ∪ -íåïðåðûâåí è ∩ -íåïðåðûâåí.Äîê-âî: Ðàññìîòðèì ïîñëåäîâàòåëüíîñòü P1 ⊆ P2 ⊆ . . .ïîäìíîæåñòâ ìíîæåñòâà S . Òàê êàê S êîíå÷íîå ìíîæåñòâî,ñóùåñòâóåò òàêîå j0 , ÷òî Pj = Pj äëÿ ëþáîãî j > j0 . Ïðè ýòîìPj ⊆ Pj äëÿ êàæäîãî j < j0 .
Характеристики
Тип файла PDF
PDF-формат наиболее широко используется для просмотра любого типа файлов на любом устройстве. В него можно сохранить документ, таблицы, презентацию, текст, чертежи, вычисления, графики и всё остальное, что можно показать на экране любого устройства. Именно его лучше всего использовать для печати.
Например, если Вам нужно распечатать чертёж из автокада, Вы сохраните чертёж на флешку, но будет ли автокад в пункте печати? А если будет, то нужная версия с нужными библиотеками? Именно для этого и нужен формат PDF - в нём точно будет показано верно вне зависимости от того, в какой программе создали PDF-файл и есть ли нужная программа для его просмотра.
![](https://s.studizba.com/z.php?f=/templates/si/i/noavatar.png&w=100&h=100&t=1"){kind=avatar}
